default search action
International Journal on Software Tools for Technology Transfer (STTT), Volume 5
Volume 5, Number 1, November 2003
- 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 A. Peled:
Compositional message sequence charts. 78-89
- Philippe Chevalley, Pascale Thévenod-Fosse:
A mutation analysis tool for Java programs. 90-103
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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.