Publications

From UclidWiki

Jump to: navigation, search

UCLID Related Publications

  • 2007
    • Formal Verification at Higher Levels of Abstraction. Daniel Kroening and Sanjit A. Seshia. Tutorial paper in 25th IEEE/ACM International Conference on Computer-Aided Design (ICCAD), November 2007. pdf
    • Symbolic Reachability Analysis of Lazy Linear Hybrid Automata. Susmit Jha, Bryan Brady, and Sanjit A. Seshia. In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), October 2007, pages 241-256. pdf
    • On Solving Boolean Combinations of UTVPI Constraints. Sanjit A. Seshia, K. Subramani, and Randal E. Bryant. In Journal of Boolean Satisfiability, Modeling, and Computation (JSAT), 2007 (to appear). pdf
    • Deciding Bit-Vector Arithmetic with Abstraction. Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady. In 13th Intl. Conference on Tools and Algorithms for the Construction of Systems (TACAS), pages 358-372, March 2007. pdf


  • 2005
    • Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. Sanjit A. Seshia. Ph.D. Thesis, Carnegie Mellon University, May 2005. html
    • Automatic Discovery of API-Level Exploits. Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, and Randal E. Bryant. 27th International Conference on Software Engineering (ICSE), 2005. ps, pdf
    • Semantics-Aware Malware Detection. Mihai Christodorescu, Somesh Jha, Sanjit A. Seshia, Dawn Song, and Randal E. Bryant. IEEE Symposium on Security and Privacy, Oakland, May 2005. pdf
    • Term-Level Verification of a Pipelined CISC Microprocessor. Randal E. Bryant. Computer Science Department Technical Report CMU-CS-05-195, December 2005. html
  • 2004
    • The UCLID Decision Procedure. Shuvendu K. Lahiri and Sanjit A. Seshia. Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 475-478, July 2004. ps, pdf
    • Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. Sanjit A. Seshia and Randal E. Bryant. Proc. of 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 100-109, July 2004. ps, pdf
    • Abstraction-based Satisfiability Solving of Presburger Arithmetic. Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, and Ofer Strichman. Proc. of Intl. Conf. on Computer-Aided Verification (CAV), LNCS 3114, pages 308-320, July 2004. ps, pdf
  • 2003
    • Deciding Quantifier-Free Presburger Formulas Using Finite Instantiation Based on Parameterized Solution Bounds. Sanjit A. Seshia and Randal E. Bryant. Computer Science Department Technical report CMU-CS-03-210, December 2003. html
    • A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions. Sanjit A. Seshia, Shuvendu K. Lahiri, and Randal E. Bryant. In Proc. 40th Design Automation Conference (DAC), ACM Press, pages 425-430, June 2003. ps, pdf
    • Convergence Testing in Term-Level Bounded Model Checking. Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. 12th Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS 2860, pages 348-362, October 2003. ps, pdf
    • Convergence Testing in Term-Level Bounded Model Checking. R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Computer Science Department Technical report CMU-CS-03-156, June 2003. html
  • 2002
    • Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002. ps, pdf
    • Deciding Separation Formulas with SAT. Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant. In Proc. Computer-Aided Verification (CAV), LNCS 2404, Copenhagen, Denmark, July 2002. ps, pdf
    • Reducing Separation Formulas to Propositional Logic. O. Strichman, S. A. Seshia, and R. E. Bryant. Computer Science Department Technical report CMU-CS-02-132, April 2002. html
    • Deciding CLU Logic Formulas via Boolean and Pseudo-Boolean Encodings. Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. In Proc. Intl. Workshop on Constraints in Formal Verification ,September 2002. Associated with Intl. Conf. on Principles and Practice of Constraint Programming. ps, pdf
    • Modeling and Verification of Out-of-Order Microprocessors using UCLID. Shuvendu K. Lahiri, Sanjit A. Seshia, and Randal E. Bryant. In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD), LNCS 2517, pages 142-159, November 2002. ps, pdf
Retrieved from "http://uclid.eecs.berkeley.edu/wiki/index.php/Publications"
Personal tools