Books
Short works
Books : reviews
Jim Woodcock, Jim Davies.
Using Z: specification, refinement, and proof.
Prentice-Hall. 1996
+
(read but not reviewed)
Jeannette M. Wing, Jim Woodcock, Jim Davies, eds.
FM'99 volume 1: World Congress on Formal Methods, Toulouse, September 1999.
Springer. 1999
(read but not reviewed)
Contents
- C. A. R. Hoare. Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle. 1999
- Cliff B. Jones. Scientific Decisions which Characterize VDM. 1999
- John M. Rushby. Mechanized Formal Methods: Where Next?. 1999
- Joseph Sifakis. Integration, the Price of Success (extended abstract). 1999
- Michael Jackson. The Role of Formalism in Method (abstract). 1999
- Eric Conquet, Jean-Luc Marty. Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project.. 1999
- Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter B. Teeuw, Chris A. Vissers. A Business Process Design Language. 1999
- Jan Philipps, Bernhard Rumpe. Refinement of Pipe-and-Filter Architectures. 1999
- John Herbert, Bruno Dutertre, Robert A. Riemenschneider, Victoria Stavridou. A Formalization of Software Architecture. 1999
- Reino Kurki-Suonio. Component and Interface Refinement in Closed-System Specifications. 1999
- Dusko Pavlovic. Semantics of First Order Parametric Specifications. 1999
- Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan. A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. 1999
- Frank Reffel, Stefan Edelkamp. Error Detection with Directed Symbolic Model Checking. 1999
- Rajeev Alur, Joel M. Esposito, M. Kim, Vijay Kumar, Insup Lee. Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination. 1999
- Stavros Tripakis, Karine Altisen. On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems. 1999
- Jean-Michel Couvreur. On-the-Fly Verification of Linear Temporal Logic. 1999
- David Deharbe, Anamaria Martins Moreira. Symbolic Model Checking with Fewer Fixpoint Computations. 1999
- Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Gigliola Vaglini. Formula Based Abstractions of Transition Systems for Real-Time Model Checking. 1999
- Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. 1999
- Farn Wang. Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes. 1999
- Denis Sabatier, Pierre Lartigue. The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications. 1999
- Patrick Behm, Paul Benoit, Alain Faivre, Jean-Marc Meynadier. Meteor: A Successful Application of B in a Large Project. 1999
- Brian Matthews, Elvira Locuratolo. Formal Development of Databases in ASSO and B. 1999
- Yann Rouzaud. Interpreting the B-Method in the Refinement Calculus. 1999
- Martin Buchi, Ralph-Johan Back. Compositional Symmetric Sharing in B. 1999
- Cesar Munoz,, John M. Rushby. Structural Embeddings: Mechanization with Method. 1999
- Steve Dunne. The Safe Machine: A New Specification Construct for B. 1999
- Michael J. Butler. csp2B: A Practical Approach to Combining CSP and B. 1999
- Salimeh Behnia, Helene Waeselynck. Test Criteria Definition for B Models. 1999
- Richard F. Paige, Eric C. R. Hehner. Bunches for Object-Oriented, Concurrent, and Real-Time Specification. 1999
- Enn Tyugu, Mihhail Matskin, Jaan Penjam. Applications of Structural Synthesis of Programs. 1999
- Michel Charpentier, K. Mani Chandy. Towards a Compositional Approach to the Design and Verification of Distributed Systems. 1999
- Andre Wong, Marsha Chechik. Formal Modeling in a Commercial Setting: A Case Study. 1999
- Igor Burdonov, Alexander Kossatchev, Alexandre Petrenko, Dmitri Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. 1999
- Lydie du Bousquet. Feature Interaction Detection Using Testing and Model-Checking Experience Report. 1999
- Nisse Husberg, Tapio Manner. Emma: Developing an Industrial Reachability Analyser for SDL. 1999
- Jean-Francois Monin, Francis Klay. Correctness Proof of the Standardized Algorithm for ABR Conformance. 1999
- Thomas Arts, Mads Dam. Verifying a Distributed Database Lookup Manager Written in Erlang. 1999
- Fred Gilham, Robert A. Riemenschneider, Victoria Stavridou. Secure Interoperation of Secure Distributed Databases. 1999
- Volkmar Lotz, Volker Kessler, Georg Walter. A Formal Security Model for Microprocessor Hardware. 1999
- Steve Schneider. Abstraction and Testing. 1999
- Dan Zhou, Shiu-Kai Chin. Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol. 1999
- Patrick Lincoln, John C. Mitchell, Mark Mitchell, Andre Scedrov. Probabilistic Polynomial-Time Equivalence and Security Analysis. 1999
- Riccardo Focardi, Fabio Martinelli. A Uniform Approach for the Definition of Security Properties. 1999
- Paul F. Syverson, Stuart G. Stubblebine. Group Principals and the Formalization of Anonymity. 1999
- Richard F. Paige, Jonathan S. Ostroff. Developing BON as an Industrial-Strength Formal Method. 1999
- Luis Mandel, Maria Victoria Cengarle. On the Expressive Power of OCL. 1999
- Eric Meyer, Jeanine Souquieres. A Systematic Approach to Transform OMT Diagrams to a B Specification. 1999
- Shaoying Liu. Verifying Consistency and Validity of Formal Specifications by Testing. 1999
- Marine Tabourier, Ana R. Cavalli, Melania Ionescu. A GSM-MAP Protocol Experiment Using Passive Testing. 1999
Jeannette M. Wing, Jim Woodcock, Jim Davies, eds.
FM'99 volume 2: World Congress on Formal Methods, Toulouse, September 1999.
Springer. 1999
(read but not reviewed)
Contents
- Pascal Poizat, Christine Choppy, Jean-Claude Royer. From Informal Requirements to COOP: A Concurrent Automata Approach. 1999
- Frederic Lang, Pierre Lescanne, Luigi Liquori. A Framework for Defining Object-Calculi. 1999
- Sanjit Arunkumar Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, S. D. Dhodapkar. A Translation of Statecharts to Esterel. 1999
- Xia Yong, Chris George. An Operational Semantics for Timed RAISE. 1999
- Heike Wehrheim. Data Abstraction for CSP-OZ. 1999
- Fiona Polack, Susan Stepney. Systems Development Using Z Generics. 1999
- full paper
- Perry Alexander, Murali Rangarajan, Phillip Baraona. A Brief Summary of VSPEC. 1999
- Gary T. Leavens, Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. 1999
- Markus Muller-Olm, Andreas Wolf. On Excusable and Inexcusable Failures. 1999
- Richard Verhoeven, Roland Carl Backhouse. Interfacing Program Construction and Verification. 1999
- S. Dellacherie, Samuel Devulder, Jean-Luc Lambert. Software Verification Based on Linear Programming. 1999
- Brendan P. Mahony, Jin Song Dong. Sensors and Actuators in TCOZ. 1999
- Bernd Krieg-Bruckner, Jan Peleska, Ernst-Rudiger Olderog, Alexander Baer. The UniForM Workbench, a Universal Development Environment for Formal Methods. 1999
- Bernhard Schatz, Franz Huber. Integrating Formal Description Techniques. 1999
- Stephan Merz. A More Complete TLA. 1999
- Frank S. de Boer, Ulrich Hannemann, Willem-Paul de Roever. Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach. 1999
- Andrew Martin. Relating Z and First-Order Logic. 1999
- Joao Pedro Sousa, David Garlan. Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework. 1999
- Leonid Mikhajlov, Emil Sekerinski, Linas Laibinis. Developing Components in the Presence of Re-entrance. 1999
- H. B. M. Jonkers. Communication and Synchronisation Using Interaction Objects. 1999
- Loe M. G. Feijs. Modelling Microsoft COM Using pi-Calculus. 1999
- Irina M. Smarandache, Thierry Gautier, Paul Le Guernic. Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints. 1999
- Simin Nadjm-Tehrani, Ove Akerlund. Combining Theorem Proving and Continuous Models in Synchronous Design. 1999
- Juliano Iyoda, Augusto Sampaio, Leila Silva. ParTS: A Partitioning Transformation System. 1999
- He Jifeng. A Behavioral Model for Co-design. 1999
- Ana L. C. Cavalcanti, David A. Naumann. A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. 1999
- Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright. Reasoning About Interactive Systems. 1999
- John Derrick, Eerke A. Boiten. Non-atomic Refinement in Z. 1999
- Eric C. R. Hehner, Andrew M. Gravell. Refinement Semantics and Loop Rules. 1999
- Michel R. V. Chaudron, Jan Tretmans, Klaas Wijbrans. Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System. 1999
- Steve King, Jonathan Hammond, Rod Chapman, Andy Pryor. The Value of Verification: Positive Experience of Industrial Proof. 1999
- Anne Elisabeth Haxthausen, Jan Peleska. Formal Development and Verification of a Distributed Railway Control System. 1999
- Kaisa Sere, Elena Troubitsyna. Safety Analysis in Formal Specification. 1999
- Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita. Formal Specification and Validation of a Vital Communication Protocol. 1999
- Herve Marchand, Mazen Samaan. Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology. 1999
- Akira Mori, Kokichi Futatsugi. Verifying Behavioural Specifications in CafeOBJ Environment. 1999
- Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida. Component-Based Algebraic Specification and Verification in CafeOBJ. 1999
- Shin Nakajima. Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. 1999
- Manuel Clavel, Fransisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr. Maude as a Formal Meta-tool. 1999
- Joseph A. Goguen, Grigore Rosu. Hiding More of Hidden Algebra. 1999
- Robert Eschbach. A Termination Detection Algorithm: Specification and Verification. 1999
- Erich Gradel, Marc Spielmann. Logspace Reducibility via Abstract State Machines. 1999
- Martin Dunstan, Tom Kelsey, Ursula Martin, Steve Linton. Formal Methods for Extensions to CAS. 1999
- Rosa M. Jimenez, Fernando Orejas. An Algebraic Framework for Higher-Order Modules. 1999
- Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen. Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. 1999
- P. Garbett, J. P. Parkes, M. Shackleton, Stuart Anderson. Secure Synthesis of Code: A Process Improvement Experiment. 1999
- Olivier Hainque, Laurent Pautet, Yann Le Biannic, Eric Nassor. Cronos: A Separate Compilation Toolset for Modular Esterel Applications. 1999
Jim Davies, A. W. Roscoe, Jim Woodcock, eds.
Millennial Perspectives in Computer Science: proceedings of the 1999 Oxford-Microsoft symposium in honour of Sir Tony Hoare.
Prentice-Hall. 2000
Contents
- Samson Abramsky. Concurrent interaction games. 2000
- Richard S. Bird, Jeremy Gibbons, Geraint Jones. Program optimisation, naturally. 2000
- Dines Bjorner. Domain modelling. 2000
- Richard P. Brent. The binary Euclidean algorithm. 2000
- Stephen Brookes. Communicating Parallel Processes. 2000
- Stephen Cameron. Computing with shapes. 2000
- K. Mani Chandy, Michel Charpentier. Predicate transformers for composition. 2000
- Ole-Johan Dahl. A note on monitor versions. 2000
- Edsger W. Dijkstra. A formula is worth a thousand pictures. 2000
- Mike J. C. Gordon. Linking higher order logic to binary decision diagrams. 2000
- David Gries, Fred B. Schneider. Substitution of equals for equals. 2000
- He Jifeng, Xu Qiwen. Advanced features of the duration calculus. 2000
- Eric C. R. Hehner. Formalism and the variable. 2000
- Michael Jackson. The real world. 2000
- Cliff B. Jones. Compositionality, interference and concurrency. 2000
- Donald E. Knuth. Dancing links. 2000
- David May. The transputer revisited. 2000
- Bertrand Meyer. Principles of language design and evolution. 2000
- Robin Milner. Computing and communication-what's the difference?. 2000
- Jayadev Misra. Generating-functions of interconnection networks. 2000
- Carroll Morgan, Annabelle McIver, J. W. Sanders. Probably Hoare? Hoare probably!. 2000
- Roger M. Needham. Distributed computing: opportunity, challenge, or misfortune?. 2000
- C.-H. L. Ong, A. S. Murawski. A linear-time algorithm for verifying MLL proof nets. 2000
- John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. 2000
- A. W. Roscoe, G. M. Reed, R. Forster. The successes and failures of behavioural models. 2000
- J. Michael Spivey, Silvija Seres. The algebra of searching. 2000
- Bernard Sufrin, Oege de Moor. Modeless structure editing. 2000
- Antti Valmari. A chaos-free failures-divergences semantics. 2000
- Niklaus Wirth. Records, modules, objects, classes, components. 2000
- Jim Woodcock, Jim Davies, Christie Bolton. Abstract data types and processes. 2000
- Zhou Chaochen, Dimitar P. Guelev, Zhan Naijun. A higher-order duration calculus. 2000