Volume 5, Number 1, November 2003
Special section on trends in verification and validation
- Tiziana Margaria, Wang Yi:
Introductory paper: scalability aspects of validation.
1-3
- Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard:
Satisfiability checking using Boolean Expression Diagrams.
4-14
- Tuba Yavuz-Kahveci, Tevfik Bultan:
A symbolic manipulator for automated verification of reactive systems with heterogeneous data types.
15-33
- Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser:
Finding feasible abstract counter-examples.
34-48
- Thomas Ball, Andreas Podelski, Sriram K. Rajamani:
Boolean and Cartesian abstraction for model checking C programs.
49-58
- Brian Nielsen, Arne Skou:
Automated test generation from timed automata.
59-77
- Elsa L. Gunter, Anca Muscholl, Doron Peled:
Compositional message sequence charts.
78-89
Regular contribution
Volume 5, Number 2-3, March 2004
- Jaco van de Pol:
Introductory paper.
105-106
- Tiziana Margaria, Bernhard Steffen:
Lightweight coarse-grained coordination: a scalable system-level approach.
107-123
- David Lugato, Céline Bigot, Yannick Valot, Jean-Pierre Gallois, Sébastien Gérard, François Terrier:
Validation and automatic test generation on UML models: the AGATHA approach.
124-139
- Alexander Pretschner, Oscar Slotosch, Ernst Aiglstorfer, Stefan Kriebel:
Model-based testing for real.
140-157
- Gordon J. Pace, Nicolas Halbwachs, Pascal Raymond:
Counter-example generation in symbolic abstract model-checking.
158-164
- María-del-Mar Gallardo, Jesús Martínez, Pedro Merino, Ernesto Pimentel:
aSPIN: A tool for abstract model checking.
165-184
- Viktor Schuppan, Armin Biere:
Efficient reduction of finite state model checking to reachability analysis.
185-204
- Thomas Arts, Clara Benac Earle, John Derrick:
Development of a verified Erlang program for resource locking.
205-220
- Conrado Daws, Marta Z. Kwiatkowska, Gethin Norman:
Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM.
221-236
- Sylvie Boldo, Marc Daumas:
Properties of two's complement floating point notations.
237-246
- Stefan Edelkamp, Stefan Leue, Alberto Lluch-Lafuente:
Directed explicit-state model checking in the validation of communication protocols.
247-267
- Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin:
Covering sharing trees: a compact data structure for parameterized verification.
268-297
Volume 5, Number 4, May 2004
- S. Purushothaman Iyer, David Hislop, Paul L. Jones, Jaime Lee, Frederick Pearce, Stephen Van Albert:
Introductory paper.
299-300
- John C. Martin:
Formal methods software engineering for the CARA system.
301-307
- Rajeev Alur, David Arney, Elsa L. Gunter, Insup Lee, Jaime Lee, Wonhong Nam, Frederick Pearce, Stephen Van Albert, Jiaxiang Zhou:
Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System.
308-319
- Raoul Praful Jetley, Cohan Carlos, S. Purushothaman Iyer:
A case study on applying formal methods to medical devices: computer-aided resuscitation algorithm.
320-330
- Eugene W. Stark:
Formally specifying CARA in Java.
331-350
- Arnab Ray, Rance Cleaveland:
Unit verification: the CARA experience.
351-369
- Luqi, Zhiwei Guan, Valdis Berzins, Lynn Zhang, David L. Floodeen, Vedat Coskun, Joseph Puett, Michael Brown:
Requirements-document-based prototyping of CARA software.
370-390
Last update Sat May 25 21:06:43 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
