10 citations · 32 across the 26 of their papers we have counts for
9 papers · 1 filter
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
Yuhao Zhou, Stavros Tripakis
The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Netw…
Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms
Derek Egolf, Stavros Tripakis
Synthesis of distributed protocols is a hard, often undecidable, problem. Completion techniques provide partial remedy by turning the problem into a search problem. However, the sp…
Decoupled Fitness Criteria for Reactive Systems
Derek Egolf, Stavros Tripakis
The correctness problem for reactive systems has been thoroughly explored and is well understood. Meanwhile, the efficiency problem for reactive systems has not received the same a…
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
William Schultz, Ian Dardik, Stavros Tripakis
We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference tec…
Comparison of Two Theorem Provers: Isabelle/HOL and Coq
Artem Yushkovskiy
The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the da…
The Refinement Calculus of Reactive Systems Toolset
Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis
We present the Refinement Calculus of Reactive Systems Toolset, an environment for compositional modeling and reasoning about reactive systems, built on top of Isabelle, Simulink,…
The Refinement Calculus of Reactive Systems
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which allows to d…
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
Hierarchical block diagrams (HBDs) are at the heart of embedded system design tools, including Simulink. Numerous translations exist from HBDs into languages with formal semantics,…
What's Decidable about Syntax-Guided Synthesis?
Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia +1
Syntax-guided synthesis (SyGuS) is a recently proposed framework for program synthesis problems. The SyGuS problem is to find an expression or program generated by a given grammar…