Sava Krstic

Email: sava dot krstic at intel dot com
Tel: (971) 214-1708

Teaching

Winter 2009: CS532 Analysis and Design of Algorithms

Publications

• Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, and Cesare Tinelli: Ground Interpolation for the Theory of Equality TACAS 2009 (Abstract) (ps, pdf )
• Amit Goel, Sava Krstic, and Alexander Fuchs: Deciding Array Formula with Frugal Axiom Instantiation SMT 2008 (Abstract) (ps, pdf )
• Sava Krstic and Amit Goel: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL FroCoS 2007 (Abstract) (ps, pdf )
• Dagstuhl slides (pdf)
• Sava Krstic, Amit Goel, Jim Grundy, and Cesare Tinelli: Combined Satisfiability Modulo Parametric Theories TACAS 2007 (Abstract) (ps, pdf )
• Mike Gordon's Festschrift talk: TTVSI (pdf)
• Sava Krstic, Jordi Cortadella, Mike Kishinevsky, and John O' Leary: Synchronous Elastic Circuits FMCAD 2006 (Abstract) (ps, pdf )
• Addendum: DCC 2008 (Ext. abstract: pdf) (Slides pdf)
• Sava Krstic, Robert Jones, and John O'Leary: Mothers of Pipelines PDPAR 2006 ENTCS, vol. 174(8): 7-22, 2007 (Abstract) (ps, pdf )
• Jim Grundy, Tom Melham, Sava Krstic, and Sean McLaughlin: Tool Building Requirements for an API to First-Order Solvers PDPAR 2005 ENTCS, vol. 144(2): 15-26, 2006 (Abstract) (pdf)
• Sava Krstic: Parametrized System Verification with Guard Strengthening and Parameter Abstraction AVIS 2005 [to appear in ENTCS] (Abstract) (preprint: ps, pdf )
• Sava Krstic and John Matthews: Semantics of the reFLect language PPDP 2004 (Abstract) (ps, pdf )
• Sava Krstic: Inductive Fixpoints in Higher Order Logic [unpublished, 2003] (Abstract) (ps, pdf )
• Sava Krstic, John Matthews: Subject Reduction and Confluence for the reFLect Language OGI Tech Report CSE-03-014, 2003 (ps, pdf )
• Sava Krstic, John Matthews: Inductive Invariants for Nested Recursion TPHOLS 2003 (Abstract) (ps, pdf ) ©Springer
• Sava Krstic, Sylvain Conchon: Canonization for Disjoint Union of Theories CADE 2003 (Abstract) (ps, pdf ) ©Springer
  • journal version (Information and Computation, vol. 199, 2005) (preprint: ps)
• Sylvain Conchon, Sava Krstic: Strategies for Combining Decision Procedures TACAS 2003 (Abstract) (ps, pdf ) ©Springer
  • journal version (Theoretical Computer Science, vol. 354, 2006) (preprint: ps )
• Sava Krstic, John Matthews: Verifying BDD Algorithms through Monadic Interpretation VMCAI 2002 (Abstract) (ps, pdf ) ©Springer
• Sava Krstic, John Launchbury, and Dusko Pavlovic: Hyperfunctions Extended Abstract FICS 2001 (ps, pdf )
• Sava Krstic, John Launchbury, and Dusko Pavlovic: Categories of Processes Enriched in Final Coalgebras FoSSaCS 2001 (Abstract) (ps, pdf ) © Springer
• John Launchbury, Sava Krstic, and Timothy E. Sauerwein: Zip Fusion with Hyperfunctions [unpublished, 2000] (Abstract) ( ps, pdf )
• Sava Krstic, Byron Cook, John Launchbury, and John Matthews: Top-level Refinement in Processor Verification [unpublished, 1999] (Abstract) (ps, pdf)
• Papers in Mathematics