@inproceedings{4463,
abstract = {We present an algorithm called TAR (“Thread-modular Abstraction Refinement”) for model checking safety properties of concurrent software. The TAR algorithm uses thread-modular assume-guarantee reasoning to overcome the exponential complexity in the control state of multithreaded programs. Thread modularity means that TAR explores the state space of one thread at a time, making assumptions about how the environment can interfere. The TAR algorithm uses counterexample-guided predicate-abstraction refinement to overcome the usually infinite complexity in the data state of C programs. A successive approximation scheme automatically infers the necessary precision on data variables as well as suitable environment assumptions. The scheme is novel in that transition relations are approximated from above, while at the same time environment assumptions are approximated from below. In our software verification tool BLAST we have implemented a fully automatic race checker for multithreaded C programs which is based on the TAR algorithm. This tool has verified a wide variety of commonly used locking idioms, including locking schemes that are not amenable to existing dynamic and static race checkers such as ERASER or WARLOCK.},
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S and Qadeer,Shaz},
pages = {262 -- 274},
publisher = {Springer},
title = {{Thread-modular abstraction refinement}},
doi = {10.1007/978-3-540-45069-6_27},
volume = {2725},
year = {2003},
}
@inproceedings{4464,
abstract = {We introduce the paradigm of schedule-carrying code (SCC). A hard real-time program can be executed on a given platform only if there exists a feasible schedule for the real-time tasks of the program. Traditionally, a scheduler determines the existence of a feasible schedule according to some scheduling strategy. With SCC, a compiler proves the existence of a feasible schedule by generating executable code that is attached to the program and represents its schedule. An SCC executable is a real-time program that carries its schedule as code, which is produced once and can be revalidated and executed with each use. We evaluate SCC both in theory and practice. In theory, we give two scenarios, of nonpreemptive and distributed scheduling for Giotto programs, where the generation of a feasible schedule is hard, while the validation of scheduling instructions that are attached to the programs is easy. In practice, we implement SCC and show that explicit scheduling instructions can reduce the scheduling overhead up to 35% and can provide an efficient, flexible, and verifiable means for compiling Giotto programs on complex architectures, such as the TTA.},
author = {Thomas Henzinger and Kirsch, Christoph M and Matic, Slobodan},
pages = {241 -- 256},
publisher = {ACM},
title = {{Schedule-carrying code}},
doi = {10.1007/978-3-540-45212-6_16},
volume = {2855},
year = {2003},
}
@inbook{4465,
abstract = {Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots.},
author = {Thomas Henzinger and Horowitz, Benjamin and Kirsch, Christoph M},
booktitle = {Software-Enabled Control: Information Technology for Dynamical Systems},
pages = {123 -- 146},
publisher = {Wiley-Blackwell},
title = {{Embedded control systems development with Giotto}},
doi = {10.1002/047172288X.ch8},
year = {2003},
}
@inproceedings{4466,
abstract = {One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternationfree fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.},
author = {Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S},
pages = {49 -- 64},
publisher = {Springer},
title = {{On the universal and existential fragments of the mu-calculus}},
doi = {10.1007/3-540-36577-X_5},
volume = {2619},
year = {2003},
}
@inproceedings{4467,
abstract = {BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification system for checking safety properties of C programs using automatic property-driven construction and model checking of software abstractions. Blast implements an abstract-model check-refine loop to check for reachability of a specified label in the program. The abstract model is built on the fly using predicate abstraction. This model is then checked for reachability. If there is no (abstract) path to the specified error label, Blast reports that the system is safe and produces a succinct proof. Otherwise, it checks if the path is feasible using symbolic execution of the program. If the path is feasible, Blast outputs the path as an error trace, otherwise, it uses the infeasibility of the path to refine the abstract model. Blast short-circuits the loop from abstraction to verification to refinement, integrating the three steps tightly through “lazy abstraction” [5]. This integration can offer significant advantages in performance by avoiding the repetition of work from one iteration of the loop to the next. },
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S and Sutre, Grégoire},
pages = {235 -- 239},
publisher = {Springer},
title = {{Software verification with BLAST}},
doi = {10.1007/3-540-44829-2_17},
volume = {2648},
year = {2003},
}