Publication
Debugging Temporal Specifications with Concept Analysis
Publications associées (69)
Path Invariants
Dirk Thilo Beyer, Andrey Rybalchenko
The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a new method for automated abstraction refinement, which overcomes the inherent limitations of predicate discovery schemes. In ...
2006VISUAL CONTRACTS: A way to reason about states and cardinalities in IT system specifications
Alain Wegmann, Lam Son Lê, José Diego de la Cruz Garcia
Visual modeling languages propose specialized diagrams to represent behaviour and concepts necessary to specify IT systems. As a result, to understand a specification, the modeller needs to analyze these two types of diagrams and, often, additional stateme ...
2006Expressing Systemic Contexts in Visual Models of System Specifications
Gil Regev, Alain Wegmann, José Diego de la Cruz Garcia
Decision support systems can be used to manage systems. Managed systems are described by system specifications. System specification notations, such as UML, often separate in different diagrams the static specification and the dynamic specification of the ...
2005The KeY Tool
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an in ...
Springer2005Detecting Malicious Code by Model Checking
The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demons ...
Springer2005Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications
The tolerance theory by Arora and Kulkarni views a fault-tolerant program as the composition of a fault-intolerant program and fault tolerance components called detectors and correctors.At its core, the theory assumes that the correctness specifications un ...
2003Modeling Consensus in a Process Calculus
Rachele Fuzzati, Massimo Merro
We give a process calculus model that formalizes a well known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors (Diamond S); we use our model to formally prove that the algorithm satisf ...
2003Modeling Consensus in a Process Calculus
Rachele Fuzzati, Massimo Merro
We give a process calculus model that formalizes a well-known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors; we use our model to formally prove that the algorithm satisfies its spec ...
2003Mining Specifications
Program verification is a promising approach to improving program quality, because it can search all possible program executions for specific errors. However, the need to formally describe correct behavior or errors is a major barrier to the widespread ado ...
ACM2002A Formal Analysis of Syverson`s Rational Exchange Protocol
Jean-Pierre Hubaux, Levente Buttyan, Srdan Capkun
In this paper, we provide a formal analysis of a rational exchange protocol proposed by Syverson. A rational exchange protocol guarantees that misbehavior cannot generate benefits, and is therefore discouraged. The analysis is performed using our formal mo ...
2002