5 papers
How Powerful are LLMs in Generating Formal Program Specifications?
Fanpeng Yang, Xing Li, Shuling Wang +7
Formal verification provides strong guarantees of software correctness, but its adoption is limited by the high cost of writing precise formal specifications. While recent large la…
STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)
Martin Jouve-Genty, Han Su, Sota Sato +3
Modern cyber-physical systems are complex, and requirements are often written in Signal Temporal Logic (STL). Writing the right STL is difficult in practice; engineers benefit from…
Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions
Shenghua Feng, Jie An, Fanjiang Xu
Stochastic dynamical systems have emerged as fundamental models across numerous application domains, providing powerful mathematical representations for capturing uncertain system…
Componentwise Automata Learning for System Integration (Extended Version)
Hiroya Fujinami, Masaki Waga, Jie An +4
Compositional automata learning is attracting attention as an analysis technique for complex black-box systems. It exploits a target system's internal compositional structure to re…
Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
Sota Sato, Jie An, Zhenya Zhang +1
We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encod…