Abstract. The Java Modeling Language (JML) recently switched to an assertion semantics based on "strong validity" in which an assertion is taken to be valid precisely whe...
We focus on synthesis techniques for transforming existing fault-intolerant real-time programs to fault-tolerant programs that provide phased recovery. A fault-tolerant program is ...
TLM (Transaction-Level Modeling) was introduced to cope with the increasing complexity of Systems-on-Chip designs by raising the modeling level. Currently, TLM is primarily used fo...
Interface automata provide a formalism capturing the high level interactions between software components. Checking compatibility, and other safety properties, in an automata-based ...
Michael Emmi, Dimitra Giannakopoulou, Corina S. Pa...
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and...
The use of formal methods can significantly improve software quality. However, many instructors and students consider formal methods to be too difficult, impractical, and esoteric ...
Declarative specifications exhibit a variety of problems, such as inadvertently overconstrained axioms and underconstrained conjectures, that are hard to diagnose with model checki...
Emina Torlak, Felix Sheng-Ho Chang, Daniel Jackson