Publications

go next top of page

Publications

[CH16]
Jürgen Christ and Jochen Hoenicke. Proof Tree Preserving Tree Interpolation. Journal of Automated Reasoning, 57(1):67–95, June 2016. [doi | Hide abstract]
Craig interpolation has a wide range of applications in model checking, verification, and state space abstraction. Recent advances use a more general version of interpolation called tree interpolation. In this paper, we present a method to extract tree interpolants from a proof tree generated by an SMT solver without modifying the proof tree. The framework is general with respect to the theories involved. We instantiate the framework to the combination of the theories of uninterpreted functions and linear arithmetic.
[HP15]
Jochen Hoenicke and Andreas Podelski. Fairness for Infinitary Control. In Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog. 2015. [doi | Hide abstract]
In 1988, Olderog and Apt developed a fair scheduler for a system with finitely many processes based on the concept of explicit scheduling. In 2010, Hoenicke, Olderog, and Podelski extended the fair scheduler from static to dynamic control. In systems with dynamic control, processes can be created dynamically. Thus, the overall number of processes can be infinite, but the number of created processes is finite at each step of an execution of the system. In this paper we extend the fair scheduler to infinitary control. In systems with infinitary control, the number of created processes can be infinite. The fair scheduler for infinitary control is perhaps interesting for its apparent unfairness: instead of treating all processes equal, the scheduler discriminates each process against finitely many other processes. However, it also privileges each process against infinitely many other processes (in fact, all but finitely many).
[FHHKP15]
Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid and Andreas Podelski. Automated Program Verification. In LATA 2015. 2015. [doi | Hide abstract]
A new approach to program verification is based on automata. The notion of automaton depends on the verification problem at hand (nested word automata for recursion, Büchi automata for termination, a form of data automata for parametrized programs, etc.). The approach is to first construct an automaton for the candidate proof and then check its validity via automata inclusion. The originality of the approach lies in the construction of an automaton from a correctness proof of a given sequence of statements. A sequence of statements is at the same time a word over a finite alphabet and it is (a very simple case of) a program. Just as we ask whether a word has an accepting run, we can ask whether a sequence of statements has a correctness proof (of a certain form). The automaton accepts exactly the sequences that do.
[CH15]
Jürgen Christ and Jochen Hoenicke. Cutting the Mix. In CAV 2015. 2015. [doi | Hide abstract]
While linear arithmetic has been studied in the context of SMT individually for reals and integers, mixed linear arithmetic allowing comparisons between integer and real variables has not received much attention. For linear integer arithmetic, the cuts from proofs algorithm has proven to have superior performance on many benchmarks. In this paper we extend this algorithm to the mixed case where real and integer variables occur in the same linear constraint. Our algorithm allows for an easy integration into existing SMT solvers. Experimental evaluation of our prototype implementation inside the SMT solver SMTInterpol shows that this algorithm is successful on benchmarks that are hard for all existing solvers.
[CH14]
Jürgen Christ and Jochen Hoenicke. Weakly Equivalent Arrays. In FroCos 2015. 2015. [doi | Hide abstract] The author's version is available at arXiv.
The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. In this paper, we present an efficient decision procedure for the theory of arrays. We build upon the notion of weak equivalence. Intuitively, two arrays are weakly equivalent if they only differ at finitely many indices. We formalise this notion and show how to exploit weak equivalences to decide formulas in the quantifier-free fragment of the theory of arrays. We present a novel data structure to represent all weak equivalence classes induced by a formula in linear space (in the number of array terms). Experimental evidence shows that this technique is competitive with other approaches.
[HHP14]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Termination Analysis by Learning Terminating Programs. In CAV 2014. Springer, 2014. [doi | Hide abstract]
We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trace is infinite but can be represented by a finite lasso. The analysis can "learn" a program from a termination proof for the lasso, a program that is terminating by construction. In a second step, the analysis checks that the set of sample traces is representative in a sense that we can make formal. An experimental evaluation indicates that the approach is a potentially useful addition to the portfolio of existing approaches to termination analysis.
[HHLP13]
Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. Linear Ranking for Linear Lasso Programs. In ATVA 2013, volume 8172 in LNCS, pages 365–380. Springer, 2013. [doi | Hide abstract] The author's version is available at arXiv.
We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trace is infinite but can be represented by a finite lasso. The analysis can "learn" a program from a termination proof for the lasso, a program that is terminating by construction. In a second step, the analysis checks that the set of sample traces is representative in a sense that we can make formal. An experimental evaluation indicates that the approach is a potentially useful addition to the portfolio of existing approaches to termination analysis.
[HHP13]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software Model Checking for People Who Love Automata. In CAV 2013, volume 8044 in LNCS, pages 36–52. Springer, 2013. Invited tutorial. [doi | Hide abstract]
In this expository paper, we use automata for software model checking in a new way. The starting point is to fix the alphabet: the set of statements of the given program. We show how automata over the alphabet of statements can help to decompose the main problem in software model checking, which is to find the right abstraction of a program for a given correctness property.
[CH13]
Jürgen Christ and Jochen Hoenicke. Extending Proof Tree Preserving Interpolation to Sequences and Trees. In SMT-workshop. 2013. [pdf | Hide abstract]
We present ongoing work to extend proof tree preserving interpolation to inductive sequences and tree interpolants. We present an algorithm to compute tree interpolants inductively over a resolution proof. Correctness of the algorithm is justified by the concept of partial tree interpolants and the appropriate definition of a projection function for conjunctions of literals onto nodes of the tree. We observe great similarities between the interpolation rules for binary interpolation and those for tree interpolation.
[CHN13]
Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. Proof Tree Preserving Interpolation. In TACAS 13, volume 7795 in LNCS, pages 126–140. Springer, 2013. [doi | technical report | improved version | Hide abstract]
Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.
[CHN12]
Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An Interpolating SMT Solver. In Model Checking Software, volume 7385 in LNCS, pages 248–254. Springer, 2012. [doi | pdf | Hide abstract]
Craig interpolation is an active research topic and has become a powerful technique in verification. We present SMTInterpol, an interpolating SMT solver for the quantifier-free fragment of the combination of the theory of uninterpreted functions and the theory of linear arithmetic over integers and reals. SMTInterpol is SMTLIB 2 compliant and available under an open source software license (LGPL v3).
[PH12]
Amalinda Post and Jochen Hoenicke. Formalization and Analysis of Real-Time Requirements: a Feasibility Study at BOSCH. In VSTTE 12, pages 225–240. Springer, 2012. [doi | pdf | Hide abstract]
In this paper, we evaluate a tool chain to algorithmically analyze real-time requirements. According to this tool chain, one formalizes the requirements in a natural-language pattern system. The requirements can then be automatically compiled into formulas in a real-time logic. The formulas can be checked automatically for properties whose violation indicates an error in the requirements specification (the properties considered are: consistency, rt-consistency, vacuity). We report on a feasibility study in the context of several automotive projects at Bosch . The results of the study indicate that the effort for the formalization of real-time requirements is acceptable; the analysis algorithms are computationally feasible; the benefit (the detection of specification errors resp. the formal guarantee of their absence) seems significant.
[EHP12]
Evren Ermis, Jochen Hoenicke, and Andreas Podelski. Splitting via Interpolants. In VMCAI 12, pages 186–201. Springer, 2012. [doi | pdf | Hide abstract]
A common problem in software model checking is the automatic computation of accurate loop invariants. Loop invariants can be derived from interpolants for every path leading through the corresponding loop header. However, in practice, the consideration of single paths often leads to very path specific interpolants. Inductive invariants can only be derived after several iterations by also taking previous interpolants into account. In this paper, we introduce a software model checking approach that uses the concept of path insensitive interpolation to compute loop invariants. In contrast to current approaches, path insensitive interpolation summarizes several paths through a program location instead of one. As a consequence, it takes the abstraction refinement considerably less effort to obtain an adequate interpolant. First experiments show the potential of our approach.
[PHP11b]
Amalinda Post, Jochen Hoenicke, and Andreas Podelski. Vacuous real-time requirements. In RE 11, pages 153–162. IEEE, 2011. [doi | pdf | Hide abstract]
We introduce the property of vacuity for requirements. A requirement is vacuous in a set of requirements if it is equivalent to a simpler requirement in the context of the other requirements. For example, the requirement ``if A then B'' is vacuous together with the requirement ``not A''. The existence of a vacuous requirement is likely to indicate an error. We give an algorithm that proves the absence of this kind of error for real-time requirements. A case study in an industrial context demonstrates the practical potential of the algorithm.
[PHP11]
Amalinda Post, Jochen Hoenicke, and Andreas Podelski. rt-inconsistency: a new property for real-time requirements. In FASE 2011, volume 6603 in LNCS, pages 34–49. Springer, 2011. [doi | pdf | Hide abstract]
We introduce rt-inconsistency, a property of real-time requirements. The property reflects that the requirements specify apparently inconsistent timing constraints. We present an algorithm to check rt-inconsistency automatically. The algorithm works via a stepwise reduction to real-time model checking. We implement the algorithm using an existing module for the reduction and the UPPAAL tool for the realtime model checking. As a case study, we apply our prototype implementation to existing real-time requirements for automotive projects at Bosch . The case study demonstrates the relevance of rt-inconsistency for detecting errors in industrial real-time requirements specifications.
[HLPSW10]
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. Doomed Program Points. Formal Methods in System Design, 37(2–3):171–199, December 2010. [doi | Hide abstract]
Any programming error that can be revealed before compiling a program saves precious time for the programmer. While integrated development environments already do a good job by detecting, e.g., data-flow abnormalities, current static analysis tools suffer from false positives ("noise") or require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if its execution will inevitably fail, regardless of which state it is started in. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on experiments with a prototype tool.
[HMO10]
Jochen Hoenicke, Roland Meyer, and E.-R. Olderog. Kleene, Rabin, and Scott are available. In CONCUR 2010, volume 6269 in LNCS, pages 462–477. Springer, 2010. [doi | pdf | Hide abstract]
We are concerned with the availability of systems, defined as the ratio between time of correct functioning and uptime. We propose to model guaranteed availability in terms of regular availability expressions (rae) and availability automata. We prove that the intersection problem of rae is undecidable. We establish a Kleene theorem that shows the equivalence of the formalisms and states precise correspondence of flat rae and simple availability automata. For these automata, we provide an extension of the powerset construction for finite automata due to Rabin and Scott. As a consequence, we can state a complementation algorithm. This enables us to solve the synthesis problem and to reduce model checking of availability properties to reachability.
[HOP10]
Jochen Hoenicke, E.-R. Olderog, and Andreas Podelski. Fairness for Dynamic Control. In TACAS 2010, volume 6015 in LNCS, pages 251–265. Springer, 2010. [doi | pdf | Hide abstract]
Already in Lamport's bakery algorithm, integers are used for fair schedulers of concurrent processes. In this paper, we present the extension of a fair scheduler from `static control' (the number of processes is fixed) to `dynamic control' (the number of processes changes during execution). We believe that our results shed new light on the concept of fairness in the setting of dynamic control.
[HHP10]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Nested Interpolants. In POPL 10, pages 471–482. ACM, 2010. [doi | pdf | Hide abstract]
In this paper, we explore the potential of the theory of nested words for partial correctness proofs of recursive programs. Our conceptual contribution is a simple framework that allows us to shine a new light on classical concepts such as Floyd/Hoare proofs and predicate abstraction in the context of recursive programs. Our technical contribution is an interpolant-based software model checking method for recursive programs. The method avoids the costly construction of the abstract transformer by constructing a nested word automaton from an inductive sequence of `nested interpolants' (i.e., interpolants for a nested word which represents an infeasible error trace).
[HLPSW09]
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. It's Doomed; we can Prove it. In FM 2009, volume 5850 in LNCS, pages 338–353. Springer, 2009. [doi | pdf | Hide 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 they require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if an execution that reaches it, in whatever state, will inevitably fail. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on preliminary experiments with a prototypical tool.
[HHP09]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Refinement of Trace Abstraction. In Static Analysis Symposium (SAS 2009), volume 5673 in LNCS, pages 69–85. Springer, 2009. [doi | pdf | Hide abstract]
Automatic refinement of abstraction is an active research theme in static analysis. In existing approaches, calls to theorem provers (for the construction of a sequence of increasingly precise state abstractions) represent an obstacle to scalability. We present an approach that aims at the reuse of theorem prover calls. The abstraction is based not on states but on traces. Each refinement extends a tuple of automata with another automaton; this automaton is derived from the interpolant-based analysis of a spurious counterexample.
[MFHR08]
Roland Meyer, Johannes Faber, Jochen Hoenicke, and Andrey Rybalchenko. Model Checking Duration Calculus: a practical approach. Formal Aspects of Computing, 20(4–5):481–505, July 2008. [doi | Hide abstract]
Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).
[HM05]
Jochen Hoenicke and Patrick Maier. Model-Checking of Specifications Integrating Processes, Data and Time. In FM 2005, volume 3582 in LNCS, pages 465–480. Springer, 2005. [doi | pdf | Hide abstract]
We present a new model-checking technique for CSP-OZ-DC, a combination of CSP, Object-Z and Duration Calculus, that allows reasoning about systems exhibiting communication, data and real-time aspects. As intermediate layer we will use a new kind of timed automata that preserve events and data variables of the specification. These automata have a simple operational semantics that is amenable to verification by a constraint-based abstraction-refinement model checker. By means of a case study, a simple elevator parameterised by the number of floors, we show that this approach admits model-checking parameterised and infinite state real-time systems.
[HO02b]
Jochen Hoenicke and Ernst-Rüdiger Olderog. CSP-OZ-DC: A Combination of Specification Techniques for Processes, Data and Time. Nordic Journal of Computing, 9(4):301–334, 2002. Appeared March 2003. [pdf | Hide abstract]
CSP-OZ-DC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. This combination is illustrated by specifying the train controller of a case study on radio controlled railway crossings. The technical contribution of the paper is a smooth integration of the underlying semantic models and its use for verifying timing properties of CSP-OZ-DC specifications. This is done by combining the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for timed automata with a new tool f2u that transforms FDR transition systems and certain patterns of Duration Calculus formulae into timed automata. This approach is illustrated by the example of a vending machine.
[HO02a]
Jochen Hoenicke and Ernst-Rüdiger Olderog. Combining Specification Techniques for Processes Data and Time. In Integrated Formal Methods, volume 2335 in Lecture Notes in Computer Science, pages 245–266. Springer, May 2002. [doi | pdf | Hide abstract]
We present a new combination CSP-OZ-DC of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. The emphasis is on a smooth integration of the underlying semantic models and its use for verifying properties of CSP-OZ-DC specifications by a combined application of the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for Timed Automata. This approach is applied to part of a case study on radio controlled railway crossings.
[Hoe01]
Jochen Hoenicke. Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC. FBT 2001, jun 2001. [pdf | Hide abstract]
We use a combination of three techniques for the specification of processes, data and time: CSP, Object-Z and Duration Calculus. Whereas the combination of CSP and Object-Z is well established by the work of C. Fischer, the integration with Duration Calculus is new. The combination is used to specify parts of a novel case study on radio controlled railway crossings.
 top of page go back

Thesis

[Hoe06]
Jochen Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, July 2006. [pdf | Hide abstract]

In this work, we present a combination of the formal methods CSP, Object-Z and Duration Calculus. Each method can describe certain aspects of a system: CSP can describe behavioural aspects, such as sequential and concurrent behaviour and synchronous communication, Object-Z complex data operations, and Duration Calculus real-time requirements. It is challenging to combine these to a unified language, CSP-OZ-DC, that takes advantage of the individual strengths of the underlying formalisms.

The semantics of CSP-OZ-DC needs to cover the basic entities of the constituent languages: events for CSP, operations and data spaces for Object-Z, and time dependent observables for Duration Calculus. We describe a particular behaviour of the system as a trajectory mapping each point in time to a valuation that provides values for all state variables. Instantaneous events are represented by rising and falling edges of Boolean state variables. The trace semantics of the full system is given as the set of all behaviours that are allowed by the CSP, the Object-Z, and the Duration Calculus part.

To facilitate the use of model checkers, we also provide an operational semantics. To this end, we introduce phase event automata, a new class of timed automata. The components of a combined specification can be translated individually into phase event automata that run in parallel to build the full system. The full system permits those behaviours that are permitted by each component automaton. We prove the soundness of the translation by showing that a behaviour is in the trace semantics of the CSP, the Object-Z, or the DC part if and only if it is accepted by the corresponding automaton.

[Hoe99]
Jochen Hoenicke. Graphische Spezifikationsspachen: Der Zusammenhang zwischen Constraint Diagrams und Real-Time Symbolic Timing Diagrams. Master's thesis, University of Oldenburg, 1999. In German. [pdf | Hide abstract]
In dieser Arbeit werden zwei graphische Spezifikationssprachen, Real-Time Symbolic Timing Diagrams (RTSTD) und Constraint Diagrams (CD), betrachtet und in Zusammenhang gebracht. Es werden die semantischen Bereiche der beiden zugrundeliegenden Formalismen TPTL und DC in Zusammenhang gebracht. Auf Grundlage einer gemeinsamen Semantik wird ein Übersetzung einer Teilklasse von CDs in RTSTDs angegeben.