Tomás E. Uribe

On-line Publications (in reverse chronological order):

Click here for a list with Abstracts

Thesis:

Abstraction-based Deductive-Algorithmic Verification of Reactive Systems. Computer Science Department, Stanford University, December 1998. Technical report STAN-CS-TR-99-1618. Abstract. Also available, an errata sheet with corrections (last update: April 29, 1999).

Research Papers:

Tomás E. Uribe. Combinations of Model Checking and Theorem Proving. In Third Intl. Workshop on Frontiers of Combining Systems, vol. 1794 of Lecture Notes in Computer Science, pp. 151-170. Springer-Verlag, March 2000 (invited talk).
Zohar Manna, Anca Browne, Henny B. Sipma and Tomás E. Uribe. Visual Abstractions for Temporal Verification. In AMAST'98, vol. 1548 of LNCS, pp. 28-41, Springer-Verlag, 1998. Abstract.
Zohar Manna, Michael A. Colón, Bernd Finkbeiner, Henny B. Sipma and Tomás E. Uribe. Abstraction and Modular Verification of Infinite-State Reactive Systems. To appear in RTSE'98, LNCS, 1998. Abstract.
Michael A. Colón and Tomás E. Uribe. Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures. In International Conference on Computer-Aided Verification, CAV'98, pp. 293-304, vol. 1427 of LNCS, Springer-Verlag, June/July 1998. Abstract. Version in PDF (Acrobat).
Nikolaj S. Bjørner, Mark E. Stickel and Tomás E. Uribe. A Practical Integration of First-Order Reasoning and Decision Procedures. In Proc. of 14th International Conference on Automated Deduction, CADE-14, pp. 101-115, vol. 1249 of LNCS, Springer-Verlag, 1997. Abstract.
Nikolaj S. Bjørner, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Deductive Verification of Real-Time Systems Using STeP. Proc. of 4th Intl. AMAST Workshop on Real-Time Systems, ARTS'97, vol. 1231 of LNCS, pp. 22-43, Springer-Verlag, May 1997. Abstract. Extended version to appear in Theoretical Computer Science.
Luca de Alfaro, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Visual Verification of Reactive Systems. In Proc. of TACAS'97, vol. 1217 of LNCS, pp. 334-350, Springer-Verlag, 1997. Abstract.
Henny B. Sipma, Tomás E. Uribe and Zohar Manna. Deductive Model Checking. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 208-219, Springer-Verlag, 1996. Extended version to appear in Formal Methods in System Design. Abstract.
Anuchit Anuchitanukul, Zohar Manna and Tomás E. Uribe. Differential BDDs. In J. van Leeuwen, ed, Computer Science Today , Lecture Notes in Computer Science, Vol. 1000, pp. 218-233, Springer-Verlag, Sep. 1995. Abstract.
Tomás E. Uribe and Mark E. Stickel. Ordered Binary Decision Diagrams and the Davis-Putnam Procedure. In First International Conference on Constraints in Computational Logics, Lecture Notes in Computer Science, Vol. 845, pages 34-49, Springer-Verlag, Munich, September 1994. Abstract.
A long version is available with extra experimental results.
Tomás E. Uribe. Sorted Unification Using Set Constraints, in 11th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 607, pages 163-177, Springer-Verlag, July 1992. Abstract.
Tomás E. Uribe, Sorted Unification and the Solution of Semi-linear Membership Constraints, Technical Report UIUCDCS-R-91-1720, University of Illinois at Urbana-Champaign, December 1991. Master's Thesis. Abstract.

STeP-Related:

Zohar Manna and the STeP group. An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. In TOOLS'98, LNCS.
Zohar Manna and the STeP group. STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 415-418, Springer-Verlag, 1996. 4-page description.
Zohar Manna and the STeP group. User's Manual for STeP: The Stanford Temporal Prover (Educational Release). Technical report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995. 138 pages.
Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover (2-page abstract). In TAPSOFT'95: Theory and Practice of Software Development, Lecture Notes in Computer Science 915, May 1995, pp. 793-794.
Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994. 44 pages.

FRAPPS-related:

FRAPPS itself is available via anonymous ftp from a.cs.uiuc.edu.

Tomás E. Uribe, Alan M. Frisch and Michael K. Mitchell, An Overview of FRAPPS: A Framework for Resolution-based Proof Procedure Systems, in 11th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 607, pages 721-725, Springer-Verlag, July 1992.
Michael K. Mitchell, Tomás E. Uribe and Alan M. Frisch, A Framework for Resolution-based Automated Proof Procedure Systems - Frapps 2.0 User's Guide, Department of Computer Science, University of Illinois at Urbana-Champaign, September 1991.
Tomás E. Uribe, Constraints in Frapps, Department of Computer Science, University of Illinois at Urbana-Champaign, September 1991.

The Stanford home page.

The Computer Science Department home page.

The Theory Division home page.