Sciweavers

CAV
2010
Springer
198views Hardware» more  CAV 2010»
13 years 7 months ago
Automatically Proving Linearizability
Abstract. This paper presents a practical automatic verification procedure for proving linearizability (i.e., atomicity and functional correctness) of concurrent data structure im...
Viktor Vafeiadis
CAV
2010
Springer
243views Hardware» more  CAV 2010»
13 years 7 months ago
libalf: The Automata Learning Framework
d Abstract) Benedikt Bollig1 , Joost-Pieter Katoen2 , Carsten Kern2 , Martin Leucker3 , Daniel Neider2 , and David R. Piegdon2 1 LSV, ENS Cachan, CNRS, 2 RWTH Aachen University, 3 ...
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern...
CAV
2010
Springer
181views Hardware» more  CAV 2010»
13 years 7 months ago
Policy Monitoring in First-Order Temporal Logic
We present an approach to monitoring system policies. As a specification language, we use an expressive fragment of a temporal logic, which can be effectively monitored. We repor...
David A. Basin, Felix Klaedtke, Samuel Müller
CAV
2010
Springer
172views Hardware» more  CAV 2010»
13 years 7 months ago
Symbolic Bounded Synthesis
Abstract. Synthesis of finite state systems from full linear time temporal logic (LTL) specifications is gaining more and more attention as several recent achievements have signi...
Rüdiger Ehlers
CAV
2010
Springer
194views Hardware» more  CAV 2010»
13 years 7 months ago
LTSmin: Distributed and Symbolic Reachability
ions of ODE models (MAPLE, GNA). On the algorithmic side (Sec. 3.2), it supports two main streams in high-performance model checking: reachability analysis based on BDDs (symbolic)...
Stefan Blom, Jaco van de Pol, Michael Weber
CAV
2010
Springer
179views Hardware» more  CAV 2010»
13 years 7 months ago
Generating Litmus Tests for Contrasting Memory Consistency Models
Well-defined memory consistency models are necessary for writing correct parallel software. Developing and understanding formal specifications of hardware memory models is a chal...
Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin
CAV
2010
Springer
146views Hardware» more  CAV 2010»
13 years 7 months ago
Fast Acceleration of Ultimately Periodic Relations
Marius Bozga, Radu Iosif, Filip Konecný
CAV
2010
Springer
158views Hardware» more  CAV 2010»
13 years 7 months ago
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
Abstract. We consider the verification of parameterized Boolean proabstractions of shared-memory concurrent programs with an unbounded number of threads. We propose that such prog...
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
CAV
2010
Springer
223views Hardware» more  CAV 2010»
13 years 7 months ago
RATSY - A New Requirements Analysis Tool with Synthesis
Formal specifications play an increasingly important role in system design-flows. Yet, they are not always easy to deal with. In this paper we present RATSY, a successor of the R...
Roderick Bloem, Alessandro Cimatti, Karin Greimel,...
CAV
2010
Springer
161views Hardware» more  CAV 2010»
13 years 7 months ago
Directed Proof Generation for Machine Code
We present the algorithms used in MCVETO (Machine-Code VErification TOol), a tool to check whether a stripped machinecode program satisfies a safety property. The verification p...
Aditya V. Thakur, Junghee Lim, Akash Lal, Amanda B...