Sciweavers

CAV
2007
Springer
113views Hardware» more  CAV 2007»
14 years 5 months ago
On Synthesizing Controllers from Bounded-Response Properties
In this paper we propose a complete chain for synthesizing controllers from high-level specifications. From real-time properties expressed in the logic MTL we generate, under boun...
Oded Maler, Dejan Nickovic, Amir Pnueli
CAV
2007
Springer
113views Hardware» more  CAV 2007»
14 years 5 months ago
Three-Valued Abstraction for Continuous-Time Markov Chains
lued Abstraction for Continuous-Time Markov Chains⋆ Joost-Pieter Katoen1 , Daniel Klink1 , Martin Leucker2 , and Verena Wolf3 RWTH Aachen University1 , TU Munich2 , University of...
Joost-Pieter Katoen, Daniel Klink, Martin Leucker,...
CAV
2007
Springer
108views Hardware» more  CAV 2007»
14 years 5 months ago
Systematic Acceleration in Regular Model Checking
Abstract. Regular model checking is a form of symbolic model checking technique for systems whose states can be represented as finite words over a finite alphabet, where regular ...
Bengt Jonsson, Mayank Saksena
CAV
2007
Springer
173views Hardware» more  CAV 2007»
14 years 5 months ago
Array Abstractions from Proofs
stractions from Proofs Ranjit Jhala1 Kenneth L. McMillan2 1 UC San Diego 2 Cadence Berkeley Laboratories We present a technique for using infeasible program paths to automatically ...
Ranjit Jhala, Kenneth L. McMillan
CAV
2007
Springer
129views Hardware» more  CAV 2007»
14 years 5 months ago
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification
Jean-Christophe Filliâtre, Claude March&eacu...
CAV
2007
Springer
159views Hardware» more  CAV 2007»
14 years 5 months ago
Boolean Abstraction for Temporal Logic Satisfiability
Alessandro Cimatti, Marco Roveri, Viktor Schuppan,...
CAV
2007
Springer
118views Hardware» more  CAV 2007»
14 years 5 months ago
C32SAT: Checking C Expressions
C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is tautological, or always defined according to the ISO C99 standard. C32...
Robert Brummayer, Armin Biere
CAV
2007
Springer
112views Hardware» more  CAV 2007»
14 years 5 months ago
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
Bounded context switch reachability analysis is a useful and efficient approach for detecting bugs in multithreaded programs. In this paper, we address the application of this app...
Ahmed Bouajjani, Séverine Fratani, Shaz Qad...
CAV
2007
Springer
98views Hardware» more  CAV 2007»
14 years 5 months ago
UPPAAL-Tiga: Time for Playing Games!
In 2005 we proposed the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The first prototy...
Gerd Behrmann, Agnès Cougnard, Alexandre Da...