Sciweavers

FM
2009
Springer
127views Formal Methods» more  FM 2009»
13 years 11 months ago
Automated Property Verification for Large Scale B Models
Michael Leuschel, Jérôme Falampin, Fa...
FM
2009
Springer
92views Formal Methods» more  FM 2009»
13 years 11 months ago
Field-Sensitive Value Analysis by Field-Insensitive Analysis
Shared and mutable data-structures pose major problems in static analysis and most analyzers are unable to keep track of the values of numeric variables stored in the heap. In this...
Elvira Albert, Puri Arenas, Samir Genaim, Germ&aac...
FM
2009
Springer
106views Formal Methods» more  FM 2009»
13 years 11 months ago
Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way
Statecharts and Petri nets are two popular visual formalisms for modelling complex systems that exhibit concurrency. Both formalisms are supported by various design tools. To enabl...
Rik Eshuis
FM
2009
Springer
95views Formal Methods» more  FM 2009»
13 years 11 months ago
It's Doomed; We Can Prove It
Abstract. Programming errors found early are the cheapest. Tools applying to the early stage of code development exist but either they suffer from false positives (“noise”) or...
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podel...
FM
2009
Springer
123views Formal Methods» more  FM 2009»
13 years 11 months ago
"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis
Abstract. Bounding resource usage is important for a number of areas, notably real-time embedded systems and safety-critical systems. In this paper, we present a fully automatic st...
Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, ...
FM
2009
Springer
105views Formal Methods» more  FM 2009»
13 years 11 months ago
Three-Valued Spotlight Abstractions
Jonas Schrieb, Heike Wehrheim, Daniel Wonisch
FM
2009
Springer
171views Formal Methods» more  FM 2009»
13 years 11 months ago
Formal Management of CAD/CAM Processes
Abstract. Systematic engineering design processes have many aspects in common with software engineering, with CAD/CAM objects replacing program code as the implementation stage of ...
Michael Kohlhase, Johannes Lemburg, Lutz Schrö...
FM
2009
Springer
164views Formal Methods» more  FM 2009»
13 years 11 months ago
The Denotational Semantics of slotted-Circus
This paper describes a complete denotational semantics, in the UTP framework, of slotted-Circus, a generic framework for reasoning about discrete timed/synchronously clocked system...
Pawel Gancarski, Andrew Butterfield
FM
2009
Springer
104views Formal Methods» more  FM 2009»
13 years 11 months ago
Verifying Information Flow Control over Unbounded Processes
Abstract. Decentralized Information Flow Control (DIFC) systems enable programmers to express a desired DIFC policy, and to have the policy enforced via a reference monitor that re...
William R. Harris, Nicholas Kidd, Sagar Chaki, Som...