Sciweavers

Share
TACAS
2000
Springer
109views Algorithms» more  TACAS 2000»
8 years 9 months ago
An Extensible Type System for Component-Based Design
Yuhong Xiong, Edward A. Lee
TACAS
2000
Springer
134views Algorithms» more  TACAS 2000»
8 years 9 months ago
Integrating Low Level Symmetries into Reachability Analysis
We present three methods for the integration of symmetries into reachability analysis. Two of them lead to perfect reduction but their runtime depends on the symmetry structure. Th...
Karsten Schmidt 0004
TACAS
2000
Springer
106views Algorithms» more  TACAS 2000»
8 years 9 months ago
Verification of Parameterized Systems Using Logic Program Transformations
Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakr...
TACAS
2000
Springer
96views Algorithms» more  TACAS 2000»
8 years 9 months ago
On Memory-Block Traversal Problems in Model-Checking Timed-Systems
Fredrik Larsson, Paul Pettersson, Wang Yi
TACAS
2000
Springer
139views Algorithms» more  TACAS 2000»
8 years 9 months ago
A Markov Chain Model Checker
Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branchin...
Holger Hermanns, Joost-Pieter Katoen, Joachim Meye...
TACAS
2000
Springer
89views Algorithms» more  TACAS 2000»
8 years 9 months ago
The PROSPER Toolkit
Abstract. The Prosper (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more f...
Louise A. Dennis, Graham Collins, Michael Norrish,...
TACAS
2000
Springer
151views Algorithms» more  TACAS 2000»
8 years 9 months ago
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking
Salsa is an invariant checker for speci cations in SAL the SCR Abstract Language. To establish a formula as an invariant without any user guidance Salsa carries out an induction pr...
Ramesh Bharadwaj, Steve Sims
TACAS
2000
Springer
149views Algorithms» more  TACAS 2000»
8 years 9 months ago
Proof General: A Generic Tool for Proof Development
This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a pr...
David Aspinall
TACAS
2000
Springer
121views Algorithms» more  TACAS 2000»
8 years 9 months ago
Using Static Analysis to Improve Automatic Test Generation
Conformance testing is still the main industrial validation technique for telecommunication protocols. The automatic construction of test cases based on the model approach is hinde...
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu
TACAS
2000
Springer
138views Algorithms» more  TACAS 2000»
8 years 9 months ago
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation
This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent...
Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norma...
books