Normal Forms for Basis-Conjugating Automorphisms of a Free Group. - Mauricio Gutierrez; Sava Krstic (Int. J. Algebra Comput., 1998)

Categories of Processes Enriched in Final Coalgebras. - Sava Krstic; John Launchbury; Dusko Pavlovic (FoSSaCS, 2001)

Verifying BDD Algorithms through Monadic Interpretation. - Sava Krstic; John Matthews (VMCAI, 2002)

Inductive Invariants for Nested Recursion. - Sava Krstic; John Matthews (TPHOLs, 2003)

Semantics of the reFLect language. - Sava Krstic; John Matthews (PPDP, 2004)

Tool Building Requirements for an API to First-Order Solvers. - Jim Grundy; Thomas F. Melham; Sava Krstic; Sean McLaughlin (PDPAR@CAV, 2005)

Canonization for disjoint unions of theories. - Sava Krstic; Sylvain Conchon (Inf. Comput., 2005)

Synchronous Elastic Circuits. - Michael Kishinevsky; Jordi Cortadella; Bill Grundmann; Sava Krstic; John O'Leary (CSR, 2006)

Synchronous Elastic Networks. - Sava Krstic; Jordi Cortadella; Michael Kishinevsky; John O'Leary (FMCAD, 2006)

Mothers of Pipelines. - Sava Krstic; Robert B. Jones; John O'Leary (PDPAR/PaUL@FLoC, 2006)

Strategies for combining decision procedures. - Sylvain Conchon; Sava Krstic (Theor. Comput. Sci., 2006)

Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. - Sava Krstic; Amit Goel (FroCoS, 2007)

Combined Satisfiability Modulo Parametric Theories. - Sava Krstic; Amit Goel; Jim Grundy; Cesare Tinelli (TACAS, 2007)

Preface. - Sava Krstic; Albert Oliveras (SMT@CAV, 2007)

Ground Interpolation for Combined Theories. - Amit Goel; Sava Krstic; Cesare Tinelli (CADE, 2009)

SMT-Based System Verification with DVF. - Amit Goel; Sava Krstic; Rebekah Leslie; Mark R. Tuttle (SMT@IJCAR, 2012)

Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. - Sylvain Conchon; Amit Goel; Sava Krstic; Alain Mebsout; Fatiha Zaïdi (CAV, 2012)

Ground interpolation for the theory of equality - Alexander Fuchs 003; Amit Goel; Jim Grundy; Sava Krstic; Cesare Tinelli (Log. Methods Comput. Sci., 2012)

Quantifier Instantiation Techniques for Finite Model Finding in SMT. - Andrew Reynolds 001; Cesare Tinelli; Amit Goel; Sava Krstic; Morgan Deters; Clark W. Barrett (CADE, 2013)

Finite Model Finding in SMT. - Andrew Reynolds 001; Cesare Tinelli; Amit Goel; Sava Krstic (CAV, 2013)

Invariants for finite instances and beyond. - Sylvain Conchon; Amit Goel; Sava Krstic; Alain Mebsout; Fatiha Zaïdi (FMCAD, 2013)

Coroutining Folds with Hyperfunctions. - John Launchbury; Sava Krstic; T. E. Sauerwein (Festschrift for Dave Schmidt, 2013)

Security of SoC firmware load protocols. - Sava Krstic; Jin Yang 006; David W. Palmer; Randy B. Osborne; Eran Talmor (HOST, 2014)

FAR-Cubicle - A new reachability algorithm for Cubicle. - Sylvain Conchon; Amit Goel; Sava Krstic; Rupak Majumdar; Mattias Roux (FMCAD, 2017)