Sciweavers

FM
2008
Springer
152views Formal Methods» more  FM 2008»
14 years 1 months ago
Constraint Prioritization for Efficient Analysis of Declarative Models
The declarative modeling language Alloy and its automatic analyzer provide an effective tool-set for building designs of systems and checking their properties. The Alloy Analyzer p...
Engin Uzuncaova, Sarfraz Khurshid
FM
2008
Springer
148views Formal Methods» more  FM 2008»
14 years 1 months ago
Precise Interval Analysis vs. Parity Games
In [?], a practical algorithm for precise interval analysis is provided for which, however, no non-trivial upper complexity bound is known. Here, we present a lower bound by showin...
Thomas Gawlitza, Helmut Seidl
FM
2008
Springer
184views Formal Methods» more  FM 2008»
14 years 1 months ago
Safe and Reliable Metro Platform Screen Doors Control/Command Systems
In this article we would like to present some recent applications of the B formal method to the development of safety critical system. These SIL3/SIL41 compliant systems have their...
Thierry Lecomte
FM
2008
Springer
157views Formal Methods» more  FM 2008»
14 years 1 months ago
Checking Well-Formedness of Pure-Method Specifications
Arsenii Rudich, Ádám Darvas, Peter M...
FM
2008
Springer
192views Formal Methods» more  FM 2008»
14 years 1 months ago
CoVaC: Compiler Validation by Program Analysis of the Cross-Product
Abstract. The paper presents a deductive framework for proving program equivalence and its application to automatic verification of transformations performed by optimizing compiler...
Anna Zaks, Amir Pnueli
FM
2008
Springer
130views Formal Methods» more  FM 2008»
14 years 1 months ago
Specification and Checking of Software Contracts for Conditional Information Flow
Abstract. Information assurance applications built according to the MILS (Multiple Independent Levels of Security) architecture often contain information flow policies that are con...
Torben Amtoft, John Hatcliff, Edwin Rodrígu...
FM
2008
Springer
110views Formal Methods» more  FM 2008»
14 years 1 months ago
A Model Checking Language for Concurrent Value-Passing Systems
Modal
Radu Mateescu, Damien Thivolle