TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Abstract. The Real-Time Calculus (RTC) [16] is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by pairs of ...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Abstract. Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems oft...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Boolean satisfiability (SAT) and its extensions are becoming a core technology for the analysis of systems. The SAT-based approach divides into three steps: encoding, preprocessin...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Abstract. We present Boom, a comprehensive analysis tool for Boolean programs. We focus in this paper on model-checking non-recursive concurrent programs. Boom implements a recent ...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
We address the problem of computing the information leakage of a system in an efficient way. We propose two methods: one based on reducing the problem to reachability, and the oth...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
STRANGER is an automata-based string analysis tool for finding and eliminating string-related security vulnerabilities in PHP applications. STRANGER uses symbolic forward and back...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with small “scratchpad” memories. The price for increase...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Deciding whether a modal formula is satisfiable with respect to a given set of (global) assumptions is a question of fundamental importance in applications of logic in computer sc...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Abstract. We present a general theory that exploits simulation relations on transition systems to obtain antichain algorithms for solving the reachability and repeated reachability...
TACAS
2010
Springer
14 years 6 months ago
2010
Springer
Abstract. We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trac...