Sciweavers

Share
SPIN
2009
Springer
10 years 4 months ago
A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks
Abstract. We present a new decision procedure for detecting property violations in pushdown models for concurrent programs that use lock-based synchronization, where each thread’...
Nicholas Kidd, Peter Lammich, Tayssir Touili, Thom...
SPIN
2009
Springer
10 years 4 months ago
Symbolic Analysis via Semantic Reinterpretation
Abstract. The paper presents a novel technique to create implementations of the basic primitives used in symbolic program analysis: forward symbolic evaluation, weakest liberal pre...
Junghee Lim, Akash Lal, Thomas W. Reps
SPIN
2009
Springer
10 years 4 months ago
Identifying Modeling Errors in Signatures by Model Checking
: Most intrusion detection systems deployed today apply misuse detection as analysis method. Misuse detection searches for attack traces in the recorded audit data using predefined...
Sebastian Schmerl, Michael Vogel, Hartmut Kön...
SPIN
2009
Springer
10 years 4 months ago
Fast, All-Purpose State Storage
Existing techniques for approximate storage of visited states in a model checker are too special-purpose and too DRAM-intensive. Bitstate hashing, based on Bloom filters, is good ...
Peter C. Dillinger, Panagiotis Manolios
SPIN
2009
Springer
10 years 4 months ago
Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis
While symmetry reduction has been established to be an important technique for reducing the search space in model checking, its application in concurrent software verification is ...
Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Cha...
SPIN
2009
Springer
10 years 4 months ago
Improving Non-Progress Cycle Checks
This paper introduces a new model checking algorithm that searches for non-progress cycles, used mainly to check for livelocks. The algorithm performs an incremental depth-first s...
David Faragó, Peter H. Schmitt
SPIN
2009
Springer
10 years 4 months ago
Tool Presentation: Teaching Concurrency and Model Checking
This paper describes a set of software tools developed for teaching concurrency and model checking. jSpin is an elementary development environment for Spin that formats and filter...
Mordechai Ben-Ari
SPIN
2009
Springer
10 years 4 months ago
Subsumer-First: Steering Symbolic Reachability Analysis
Abstract. Symbolic reachability analysis provides a basis for the verification of software systems by offering algorithmic support for the exploration of the program state space ...
Andrey Rybalchenko, Rishabh Singh
SPIN
2009
Springer
10 years 4 months ago
Experience with Model Checking Linearizability
Martin T. Vechev, Eran Yahav, Greta Yorsh
books