Decision Procedures and Plugins

Stålmarck's Method in Many Sorted First Order Logic Lars Lundgren Master's thesis, Chalmers Technical University and Prover Technology, 1999. Stålmarck's method with extensions to Quantified Boolean Formulas Gunnar Stålmarck Proceedings of the Eleventh International Conference on Computer Aided Verification, Trento, Italy, July 1999, Lecture Notes in Computer Science volume 1633 (Springer-Verlag, 1999). A HOL Conversion for Translating Linear Time Temporal Logic to Omega-Automata K. Schneider and D. W. Hoffmann Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, Nice, France, 14-17 September, 1999, Lecture Notes in Computer Science volume 1690 (Springer-Verlag, 1999). Programming combinations of deduction and BDD-based symbolic calculation Mike Gordon University of Cambridge Computer Laboratory Technical Report No. 480. Available from here. Combining the Hol98 Proof Assistant with the BuDDy BDD package Mike Gordon and Ken Friis Larsen University of Cambridge Computer Laboratory Technical Report No. 481. Available from here.

Hardware Verification

Using Boolean Decomposition for Automatic Error Correction of Combinatorial Circuits Dirk Hoffmann and Thomas Kropf Technical Report 6/98, University of Karlsruhe, 1998. Verification of a GF(2m) Multiplier-Circuit for Digital Signal Processing Dirk Hoffmann and Thomas Kropf Technical Report 22/98, University of Karlsruhe, 1998. AC/3 V1.00 - A Tool for Automatic Error Correction of Combinatorial Circuits Dirk Hoffmann and Thomas Kropf Technical Report 5/99, University of Karlsruhe, 1999. Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction D. W. Hoffmann and Thomas Kropf Proceedings of the 10th IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Bad Herrenalb, Germany, September 1999, Lecture Notes in Computer Science volume 1703 (Springer-Verlag, 1999).

Natural Language Interface

ALVEY to CTL translation - a preparatory study for a finite-state verification Natural Language interface Danny Tidhar MSc dissertation, Department of Linguistics, University of Edinburgh, 1998. A semantically-derived subset of English for hardware verification Alexander Holt and Ewan Klein Proceedings of the 37th Annual Meeting of the Association for Computational Linguistics, University of Maryland, College Park, Maryland, USA, June 1999, pages 451-456 (Association for Computational Linguistics, 1999). ISBN 1-55860-609-2. Natural language for hardware verification: semantic interpretation and model checking Alexander Holt, Ewan Klein and Claire Grover Proceedings of ICoS-1 workshop: Inference in Computational Semantics, Institute for Logic, Language and Computation (ILLC), Amsterdam, August 1999, pages 133-137 (ILLC, University of Amsterdam, 1999). From Event-Based Semantics to Linear Temporal Logic: The Logical and Computational Aspects of a Natural Language Interface for Hardware Verification Tom Laureys MSc dissertation, School of Cognitive Science, University of Edinburgh, 1999. Formal verification with natural language specifications: guidelines, experiments and lessons so far Alexander Holt South African Computer Journal, No. 24, November 1999, pp. 253-257. (Special issue: Proceedings of the Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists: 17-19 November 1999, Mount Amanzi Lodge, Hartebeespoort, South Africa.)