10 citations · 32 across the 26 of their papers we have counts for
6 papers · 1 filter
Counterexample Classification
Cole Vick, Eunsuk Kang, Stavros Tripakis
In model checking, when a given model fails to satisfy the desired specification, a typical model checker provides a counterexample that illustrates how the violation occurs. In ge…
Automated Synthesis of Secure Platform Mappings
Eunsuk Kang, Stephane Lafortune, Stavros Tripakis
System development often involves decisions about how a high-level design is to be implemented using primitives from a low-level platform. Certain decisions, however, may introduce…
Type Inference of Simulink Hierarchical Block Diagrams in Isabelle
Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis
Simulink is a de-facto industrial standard for the design of embedded systems. In previous work, we developed a compositional analysis framework for Simulink models in Isabelle --…
Translating Hierarchical Block Diagrams into Composite Predicate Transformers
Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis
Simulink is the de facto industrial standard for designing embedded control systems. When dealing with the formal verification of Simulink models, we face the problem of translatin…
Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems
Viorel Preoteasa, Stavros Tripakis
Feedback is an essential composition operator in many classes of reactive and other systems. This paper studies feedback in the context of compositional theories with refinement. S…
Refinement Calculus of Reactive Systems
Viorel Preoteasa, Stavros Tripakis
Refinement calculus is a powerful and expressive tool for reasoning about sequential programs in a compositional manner. In this paper we present an extension of refinement calculu…