Research fields of UEDA Lab.

Programming Languages for Verified Software

university website  selected publications

Our research goal is to develop a framework for computation and programming that adequately addresses 21st-century computing platforms. While computing platforms currently available offer various forms of non-sequential processing capabilities and opportunities for interesting novel applications, software technologies for programming those platforms (for all stages including modeling, coding, testing and verification) are not keeping pace.

With this in mind, we are currently conducting the following three projects:

• Project LMNtal: Unifying language and system based on (hyper)graph rewriting,
• Project HPV: High-Performance Verification,
• Project HydLa: Language and system for cyber-physical systems.

Project LMNtal: Modeling and programming language based on graph rewriting, with applications to AI and computer-aided verification

LMNtal website

Our first step toward the goal of "Programming Language for Verified Software" is LMNtal (pronounced "elemental"), a unifying model and programming language based on hierarchical graph rewriting. Hierarchical graphs are a data structure that integrates two major mechanisms for structuring information, connectivity and hierarchy, and provide a powerful means of data and knowledge representation.

LMNtal was designed as a substrate model of concurrency and its embodiment as a concrete programming language. While maintaining this conception, the language and its implementation have now evolved into a framework for state-space search and model checking of non-deterministic systems and acquired many useful new applications.

Our publicly available LMNtal system and its IDE (integrated development environment) called LaViT offers a number of unique features: no discrepancy between programming and modeling languages; powerful data structures including hypergraphs and nested multisets; state and state-space visualization; scalable parallel model checking, and so forth. The system is useful not only for bug identification, but for achieving an understanding of non-deterministic concurrent systems. We believe that constructing verified software systems is not our ultimate goal; our real goal is to costruct them in a clear, understandable manner, and addressing this ultimate goal is exactly why we actively conduct the LMNtal project.

Project HPV: High-performance verification

The second research topic is high-performance verification, which refers to high-performance parallel computing applied to computer-aided verification. We believe that the power of parallel computing available today is well worth devoting to enhancing the reliability of software as a social infrastructure.

We have been developing technologies for parallelizing SAT (propositional satisfiability) solvers and model checking, both highly irregular compared to other parallel applications.

Our parallel model checker for the modeling language LMNtal now allow you to verify systems with up to two billion (~ 2^31) states, exploiting the power of recent standard SMP (symmetric multiprocessing) platforms with tens of cores and hundreds of gigabytes of memory. The use of graph rewriting as a modeling language poses many challenges including graph isomorphism checking in state-space construction, but a combination of several techniques makes graph-based model checking very practical.

Project HydLa: Constraint programming for hybrid systems

The third topic is the development of constraint-based technologies for modeling and verifying hybrid systems, namely systems involving both continuous and discrete changes. Many physical and biological systems are naturally modeled as hybrid systems, but the study of modeling from the perspective of high-level programming languages has been left unexplored.

Our approach to hybrid systems builds upon the Constraint Programming paradigm, a paradigm of computing with partial information developed at the intersection of declarative programming and artificial intelligence. We seek to establish a foundational, constraint-based framework for modeling and reasoning about hybrid systems.

The first embodiment of the above challenge is a modeling language HydLa and its implementation HyLaGI, both coming with several unique features. The key feature of HydLa is that its ingredients consist of popular mathematical and logical notions such as (in)equations, derivatives, logical implications and temporal operators. Constraint hierarchy allows you to describe both default and exceptional behaviors of a system in a concise manner.

HyLaGI is an implementation of HydLa that allows symbolic execution (simulation) of systems described in HydLa. This has several consequences: Firstly, HyLaGI is able to handle parameterized hybrid systems and systems with uncertainties. Secondly, it nondeterministically explores qualitatively different trajectories that are free from numerical errors. Thirdly, symbolic parameters serve as a useful tool for describing and reasoning about systems with subtle, intricate behaviors.

We are actively exploring the viability of HydLa and HyLaGI towards a novel tool for cyber-physical systems.