Sciweavers

SEFM
2007
IEEE
14 years 6 months ago
Sound reasoning about unchecked exceptions
Bart Jacobs 0002, Peter Müller, Frank Piessen...
SEFM
2007
IEEE
14 years 6 months ago
Verifying the Mondex Case Study
The Mondex Case study is still the most substantial contribution to the Grand Challenge repository. It has been the target of a number of formal verification efforts. Those effor...
Peter H. Schmitt, Isabel Tonin
SEFM
2007
IEEE
14 years 6 months ago
Verifying Security Properties of Cryptoprotocols: A Novel Approach
We model security protocols as a game tree using concepts of game semantics. Using this model we ascribe semantics to protocols written in the standard simple arrow notation. Acco...
Mohamed Saleh, Mourad Debbabi
SEFM
2007
IEEE
14 years 6 months ago
Hardness for Explicit State Software Model Checking Benchmarks
Directed model checking algorithms focus computation resources in the error-prone areas of concurrent systems. The algorithms depend on some empirical analysis to report their per...
Neha Rungta, Eric G. Mercer
SEFM
2007
IEEE
14 years 6 months ago
Supporting Proof in a Reactive Development Environment
Reactive integrated development environments for software engineering have lead to an increase in productivity and quality of programs produced. They have done so by replacing the...
Farhad Mehta
SEFM
2007
IEEE
14 years 6 months ago
Disciplining Orchestration and Conversation in Service-Oriented Computing
We give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when in...
Ivan Lanese, Francisco Martins, Vasco Thudichum Va...
SEFM
2007
IEEE
14 years 6 months ago
Automatically Proving Concurrent Programs Correct
of abstract interpretations in formal methods It is always very satisfying to hear about a theory, in the case at hand it is the theory of abstract interpretations, that explains i...
Byron Cook
SEFM
2007
IEEE
14 years 6 months ago
Run-time Composition and Adaptation of Mismatching Behavioural Transactions
Reuse of software entities such as components or web services raise composition issues since, most of the time, they present mismatching behavioural interfaces. Here, we particula...
Javier Cámara, Gwen Salaün, Carlos Can...