Sciweavers

Share
TACAS
2010
Springer
255views Algorithms» more  TACAS 2010»
8 years 2 months ago
Satisfiability Modulo the Theory of Costs: Foundations and Applications
Abstract. We extend the setting of Satisfiability Modulo Theories (SMT) by introducing a theory of costs C, where it is possible to model and reason about resource consumption and ...
Alessandro Cimatti, Anders Franzén, Alberto...
TACAS
2010
Springer
156views Algorithms» more  TACAS 2010»
8 years 2 months ago
Preemption Sealing for Efficient Concurrency Testing
The choice of where a thread scheduling algorithm preempts one thread in order to execute another is essential to reveal concurrency errors such as atomicity violations, livelocks,...
Thomas Ball, Sebastian Burckhardt, Katherine E. Co...
TACAS
2010
Springer
212views Algorithms» more  TACAS 2010»
8 years 2 months ago
Assume-Guarantee Verification for Probabilistic Systems
Abstract. We present a compositional verification technique for systems that exhibit both probabilistic and nondeterministic behaviour. We adopt an assume-guarantee approach to ver...
Marta Z. Kwiatkowska, Gethin Norman, David Parker,...
TACAS
2010
Springer
160views Algorithms» more  TACAS 2010»
8 years 2 months ago
Efficient Detection of Errors in Java Components Using Random Environment and Restarts
Software model checkers are being used mostly to discover specific types of errors in the code, since exhaustive verification of complex programs is not possible due to state explo...
Pavel Parizek, Tomás Kalibera
TACAS
2010
Springer
170views Algorithms» more  TACAS 2010»
8 years 2 months ago
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems
Systems and protocols combining concurrency and infinite state space occur quite often in practice, but are very difficult to verify automatically. At the same time, if the system ...
Klaus Dräger, Andrey Kupriyanov, Bernd Finkbe...
TACAS
2010
Springer
151views Algorithms» more  TACAS 2010»
8 years 2 months ago
A Polymorphic Intermediate Verification Language: Design and Logical Encoding
Abstract. Intermediate languages are a paradigm to separate concerns in software verification systems when bridging the gap between programming languages and the logics understood ...
K. Rustan M. Leino, Philipp Rümmer
TACAS
2010
Springer
316views Algorithms» more  TACAS 2010»
8 years 2 months ago
JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution
We introduce JTorX, a tool for model-driven test derivation and execution, based on the ioco theory. This theory, originally presented in [12], has been refined in [13] with test-...
Axel Belinfante
TACAS
2010
Springer
251views Algorithms» more  TACAS 2010»
8 years 9 months ago
Approximating the Pareto Front of Multi-criteria Optimization Problems
We propose a general methodology for approximating the Pareto front of multi-criteria optimization problems. Our search-based methodology consists of submitting queries to a constr...
Julien Legriel, Colas Le Guernic, Scott Cotton, Od...
TACAS
2010
Springer
342views Algorithms» more  TACAS 2010»
8 years 11 months ago
SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata
We study the model checking problem of timed automata based on SAT solving. Our work investigates alternative possibilities for coding the SAT reductions that are based on parallel...
Janusz Malinowski, Peter Niebert
TACAS
2010
Springer
169views Algorithms» more  TACAS 2010»
8 years 11 months ago
On Weak Modal Compatibility, Refinement, and the MIO Workbench
Sebastian S. Bauer, Philip Mayer, Andreas Schroede...
books