CAV
2010
Springer
14 years 18 days ago
2010
Springer
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...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
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...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
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)...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
Well-defined memory consistency models are necessary for writing correct parallel software. Developing and understanding formal specifications of hardware memory models is a chal...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
CAV
2010
Springer
14 years 18 days ago
2010
Springer
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...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
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...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
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...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
For efficiency and portability, network packet processing code is typically written in low-level languages and makes use of bit-level operations to compactly represent data. Althou...
CAV
2010
Springer
14 years 18 days ago
2010
Springer
Abstract. We propose a purely implicit solution to the contextual assumption generation problem in assume-guarantee reasoning. Instead of improving the L∗ algorithm — a learnin...