Publications 2000
- Penny Anderson and David Basin.
Program Development Schemata as Derived Rules.
In Journal of Symbolic Computation, 30 (1), pages 5-36, 2000.
[Download abstract (TXT, 868 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 343 KB) | Download gzip'ed Postscript (GZ, 140 KB)]
- Abdelwaheb Ayari and David Basin.
Bounded Model Construction for Monadic Second-Order Logics.
In 12th International Conference on Computer-Aided Verification (CAV'00).
Lecture Notes in Computer Science, 1855. Springer-Verlag, 2000.
[Download abstract (TXT, 960 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 235 KB) | Download gzip'ed Postscript (GZ, 97 KB)]
- Abdelwaheb Ayari and David Basin and Felix Klaedtke.
Decision Procedures for Inductive Boolean Functions based on Alternating Automata.
In 12th International Conference on Computer-Aided Verification (CAV'00).
Lecture Notes in Computer Science, 1855. Springer-Verlag, 2000.
[Download abstract (TXT, 760 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 240 KB) | Download gzip'ed Postscript (GZ, 103 KB)]
- David Basin and Manuel Clavel and Josè Meseguer.
Rewriting Logic as a Metalogical Framework.
In Foundations of Software Technology and Theoretical Computer Science (FSTTCS).
Lecture Notes in Computer ScienceSpringer-Verlag, 2000.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download gzip'ed Postscript (GZ, 105 KB)]
- David Basin and Stefan Friedrich.
Combining WS1S and HOL.
In Frontiers of Combining Systems 2. Research Studies Press/Wiley, 2000.
[Download abstract (TXT, 762 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 229 KB) | Download gzip'ed Postscript (GZ, 94 KB)]
- David Basin and Stefan Friedrich and Sebastian Mödersheim.
B2M: A Semantic Based Tool for BLIF Hardware Descriptions.
In Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000.
Lecture Notes in Computer Science, 1954. Springer-Verlag, 2000.
[Download abstract (TXT, 835 Bytes) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 261 KB) | Download gzip'ed Postscript (GZ, 89 KB)]
- David Basin and Luca Viganò.
A Recipe for the Complexity Analysis of Non-Classical Logics.
In Frontiers of Combining Systems 2 (Proceedings of FroCoS'98).
Studies in Logic and Computation Research Studies Press/Wiley, 2000.
[Download abstract (TXT, 758 Bytes) | Download BibTeX (TXT, 1 KB)]
- David Basin and Luca Viganò and Burkhart Wolff.
Berichte aus den Instituten: Lehrstuhl für Softwaretechnik und Softwareproduktionsumgebung, Freiburg.
In PIK (Praxis der Informationsverarbeitung und Kommunikation), 23 (4), pages 248-249, 2000.
[Download BibTeX (TXT, 584 Bytes) | Download PDF (PDF, 90 KB) | Download gzip'ed Postscript (GZ, 30 KB) | Download English translation (GZ, 27 KB)]
- Ian Frank and David Basin and Alan Bundy.
Combining Knowledge and Search to Solve Single-Suit Bridge.
In AAAI-2000.AAAI-Press, 2000.
[Download BibTeX (TXT, 334 Bytes) | Download gzip'ed Postscript (GZ, 62 KB)]
- Christoph Lüth and Burkhart Wolff.
More about TAS and IsaWin: Tools for Formal Program Development.
In Fundamental Approaches to Software Engineering FASE 200. Joint European Conferences on Theory and Practice of Software ETAPS 2000.
Lecture Notes in Computer Science, 1783. Springer Verlag, 2000.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 3.4 MB) | Download gzip'ed PDF (GZ, 92 KB)]
- Christoph Lüth and Burkhart Wolff.
TAS - A Generic Window Inference System.
In Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000.Lecture Notes in Computer Science, 1869. Springer Verlag, 2000.
[Download abstract (TXT, 838 Bytes) | Download BibTeX (TXT, 3 KB) | Download PDF (PDF, 4.7 MB) | Download gzip'ed Postscript (GZ, 224 KB)]
- T. Meyer and Burkhart Wolff.
Correct Code-Generation in a Generic Framework.
In TPHOLs 2000: Supplemental Proceedings.OGI Technical Report CSE 00-009, 2000.
[Download abstract (TXT, 800 Bytes) | Download BibTeX (TXT, 3 KB) | Download PDF (PDF, 261 KB) | Download gzip'ed Postscript (GZ, 89 KB)]
- Luca Viganò.
An O(n log n)-space decision procedure for the relevance logic B+.
In Studia Logica, 66 (3), pages 385-407, 2000.
[Download abstract (TXT, 597 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 825 KB) | Download gzip'ed Postscript (GZ, 103 KB) | Extended version: Technical report No. 140]
- G. Wimmel and H. Lötzbeyer and A. Pretschner and O. Slotosch.
Specification Based Test Sequence Generation with Propositional Logic.
In Software Testing, Validation, and Reliability, 10 (4), pages 229-248, 2000.
[Download BibTeX (TXT, 437 Bytes) | external page Wiley]
- Luca Viganò
Labelled Non-Classical Logics.
Kluwer Academic Publishers, 2000.
[Download abstract (TXT, 1019 Bytes) | Download BibTeX (TXT, 1 KB) | Download additional information (JPEG, 57 KB)]
- David Basin and Marcello D'Agostino and Dov M. Gabbay and Seán Matthews and Luca Viganò
Labelled Deduction.
Kluwer Academic Publishers, 2000.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download additional information (JPEG, 87 KB)]