@inproceedings{4452, abstract = {We describe Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers support for automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation, Gröbner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate them on examples.}, author = {Thomas Henzinger and Hottelier, Thibaud and Kovács, Laura}, pages = {333 -- 342}, publisher = {Springer}, title = {{Valigator: A verification tool with bound and invariant generation}}, doi = {10.1007/978-3-540-89439-1_24}, volume = {5330}, year = {2008}, } @article{4509, abstract = {I discuss two main challenges in embedded systems design: the challenge to build predictable systems, and that to build robust systems. I suggest how predictability can be formalized as a form of determinism, and robustness as a form of continuity.}, author = {Thomas Henzinger}, journal = {Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences}, number = {1881}, pages = {3727 -- 3736}, publisher = {Royal Society of London}, title = {{Two challenges in embedded systems design: Predictability and robustness}}, doi = {10.1098/rsta.2008.0141}, volume = {366}, year = {2008}, } @inproceedings{4521, abstract = {The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, the current focus of liveness verification has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite programexecution. In this paper, we propose a method to search for such counterexamples. The search proceeds in two phases. We first dynamically enumerate lasso-shaped candidate paths for counterexamples, and then statically prove their feasibility. We illustrate the utility of our nontermination prover, called TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations.}, author = {Ashutosh Gupta and Thomas Henzinger and Majumdar, Ritankar S and Rybalchenko, Andrey and Xu, Ru-Gang}, pages = {147 -- 158}, publisher = {ACM}, title = {{Proving non-termination}}, doi = {10.1145/1328438.1328459}, year = {2008}, } @phdthesis{4524, abstract = {Complex requirements, time-to-market pressure and regulatory constraints have made the designing of embedded systems extremely challenging. This is evident by the increase in effort and expenditure for design of safety-driven real-time control-dominated applications like automotive and avionic controllers. Design processes are often challenged by lack of proper programming tools for specifying and verifying critical requirements (e.g. timing and reliability) of such applications. Platform based design, an approach for designing embedded systems, addresses the above concerns by separating requirement from architecture. The requirement specifies the intended behavior of an application while the architecture specifies the guarantees (e.g. execution speed, failure rate etc). An implementation, a mapping of the requirement on the architecture, is then analyzed for correctness. The orthogonalization of concerns makes the specification and analyses simpler. An effective use of such design methodology has been proposed in Logical Execution Time (LET) model of real-time tasks. The model separates the timing requirements (specified by release and termination instances of a task) from the architecture guarantees (specified by worst-case execution time of the task). This dissertation proposes a coordination language, Hierarchical Timing Language (HTL), that captures the timing and reliability requirements of real-time applications. An implementation of the program on an architecture is then analyzed to check whether desired timing and reliability requirements are met or not. The core framework extends the LET model by accounting for reliability and refinement. The reliability model separates the reliability requirements of tasks from the reliability guarantees of the architecture. The requirement expresses the desired long-term reliability while the architecture provides a short-term reliability guarantee (e.g. failure rate for each iteration). The analysis checks if the short-term guarantee ensures the desired long-term reliability. The refinement model allows replacing a task by another task during program execution. Refinement preserves schedulability and reliability, i.e., if a refined task is schedulable and reliable for an implementation, then the refining task is also schedulable and reliable for the implementation. Refinement helps in concise specification without overloading analysis. The work presents the formal model, the analyses (both with and without refinement), and a compiler for HTL programs. The compiler checks composition and refinement constraints, performs schedulability and reliability analyses, and generates code for implementation of an HTL program on a virtual machine. Three real-time controllers, one each from automatic control, automotive control and avionic control, are used to illustrate the steps in modeling and analyzing HTL programs.}, author = {Ghosal, Arkadeb}, pages = {1 -- 210}, publisher = {University of California, Berkeley}, title = {{A hierarchical coordination language for reliable real-time tasks}}, year = {2008}, } @inproceedings{4527, abstract = {We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification. We use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings.}, author = {Fisher, Jasmin and Thomas Henzinger and Maria Mateescu and Piterman, Nir}, pages = {17 -- 32}, publisher = {Springer}, title = {{Bounded asynchrony: Concurrency for modeling cell-cell interactions}}, doi = {10.1007/978-3-540-68413-8_2}, volume = {5054}, year = {2008}, } @article{4532, abstract = {We consider the equivalence problem for labeled Markov chains (LMCs), where each state is labeled with an observation. Two LMCs are equivalent if every finite sequence of observations has the same probability of occurrence in the two LMCs. We show that equivalence can be decided in polynomial time, using a reduction to the equivalence problem for probabilistic automata, which is known to be solvable in polynomial time. We provide an alternative algorithm to solve the equivalence problem, which is based on a new definition of bisimulation for probabilistic automata. We also extend the technique to decide the equivalence of weighted probabilistic automata.}, author = {Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François}, journal = {International Journal of Foundations of Computer Science}, number = {3}, pages = {549 -- 563}, publisher = {World Scientific Publishing}, title = {{Equivalence of labeled Markov chains}}, doi = {10.1142/S0129054108005814 }, volume = {19}, year = {2008}, } @inproceedings{4533, abstract = {Interface theories have been proposed to support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, maintaining compatibility. We show that these interface theories provide no formal support for component reuse, meaning that the same component cannot be used to implement several different interfaces in a design. We add a new operation to interface theories in order to support such reuse. For example, different interfaces for the same component may refer to different aspects such as functionality, timing, and power consumption. We give both stateless and stateful examples for interface theories with component reuse. To illustrate component reuse in interface-based design, we show how the stateful theory provides a natural framework for specifying and refining PCI bus clients.}, author = {Doyen, Laurent and Thomas Henzinger and Jobstmann, Barbara and Tatjana Petrov}, pages = {79 -- 88}, publisher = {ACM}, title = {{Interface theories with component reuse}}, doi = {10.1145/1450058.1450070}, year = {2008}, } @article{4534, abstract = {A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives, and mean-payoff (or limit-average) objectives. These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of stochastic parity games to stochastic mean-payoff games.}, author = {Krishnendu Chatterjee and Thomas Henzinger}, journal = {Information Processing Letters}, number = {1}, pages = {1 -- 7}, publisher = {Elsevier}, title = {{Reduction of stochastic parity to stochastic mean-payoff games}}, doi = {10.1016/j.ipl.2007.08.035}, volume = {106}, year = {2008}, } @inproceedings{4546, abstract = {We propose the notion of logical reliability for real-time program tasks that interact through periodically updated program variables. We describe a reliability analysis that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The resulting analysis can be combined with an incremental schedulability analysis for interacting real-time tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination language for distributed real-time systems. We implemented a logical-reliability-enhanced prototype of the compiler and runtime infrastructure for HTL.}, author = {Krishnendu Chatterjee and Ghosal, Arkadeb and Thomas Henzinger and Iercan, Daniel and Kirsch, Christoph M and Pinello, Claudio and Sangiovanni-Vincentelli, Alberto}, pages = {909 -- 914}, publisher = {IEEE}, title = {{Logical reliability of interacting real-time tasks}}, doi = {10.1145/1403375.1403595}, year = {2008}, } @article{4548, abstract = {The value of a finite-state two-player zero-sum stochastic game with limit-average payoff can be approximated to within ε in time exponential in a polynomial in the size of the game times polynomial in logarithmic in 1/ε, for all ε > 0.}, author = {Krishnendu Chatterjee and Majumdar, Ritankar S and Thomas Henzinger}, journal = {International Journal of Game Theory}, number = {2}, pages = {219 -- 234}, publisher = {Springer}, title = {{Stochastic limit-average games are in EXPTIME}}, doi = {10.1007/s00182-007-0110-5}, volume = {37}, year = {2008}, } @inproceedings{4568, abstract = {We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking.}, author = {Beyer, Dirk and Thomas Henzinger and Théoduloz, Grégory}, pages = {29 -- 38}, publisher = {ACM}, title = {{Program analysis with dynamic change of precision}}, doi = {10.1109/ASE.2008.13}, year = {2008}, } @article{517, author = {Barton, Nicholas H}, journal = {Genetics Research}, number = {5-6}, pages = {475 -- 477}, publisher = {Cambridge University Press}, title = {{Identity and coalescence in structured populations: A commentary on 'Inbreeding coefficients and coalescence times' by Montgomery Slatkin}}, doi = {10.1017/S0016672308009683}, volume = {89}, year = {2008}, }