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...
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...
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...
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, ...
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ö...
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...
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...