Publications
[ CS CMU Publication Archive | Papers from H/W Verification Group @ Stanford ]
Publications in BibTeX format.
2004
Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, and David L. Dill. A Practical Approach to Partial Functions in CVC Lite. //In proceedings of PDPAR'04, July 2004 (Postscript)
Clark Barrett and Sergey Berezin. CVC Lite: A New Implementation of the Cooperating Validity Checker. //In Proceedings of CAV'04, July 2004 (Postscript)
Jacob Chang, Sergey Berezin, and David L. Dill. Using Interface Refinement to Integrate Formal Verification into the Design Cycle. //In Proceedings of CAV'04, July 2004 (Postscript)
2003
Clark Barrett and Sergey Berezin. A Proof-Producing Boolean Search Engine. //In Proceedings of PDPAR 2003 Workshop, Miami, Florida, USA, July, 2003. (Postscript)
Husam Abu-Haimed, Sergey Berezin and David L. Dill. Strengthening Invariants by Symbolic Consistency Testing. //In proceedings of CAV'03, July 2003. (C) 2003 Springer Verlag// (Postscript, Slides in PowerPoint)
Sergey Berezin, Vijay Ganesh, and David L. Dill. An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. //in Proceedings of TACAS'03, LNCS 2619, Warshaw, Poland, April 2003. (C) 2003 Springer Verlag// (Postscript)
- Sergey Berezin, Vijay Ganesh, and David L. Dill. Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. // Draft of a technical report, to appear soon. Stanford University, 2003.// (Postscript)
2002
Vijay Ganesh, Sergey Berezin, and David L. Dill. Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. //In proceedings of FMCAD'02, LNCS 2517, November 2002. (C) 2002 Springer Verlag// (Gzip'ed Postscript, Postscript, Slides in PowerPoint)
Sergey Berezin. Model Checking and Theorem Proving: a Unified Framework. //Ph.D. Thesis, Carnegie Mellon University, 2002. Also a TR number CMU-CS-02-100.// (Postscript, PDF) See also my thesis page for the related documents.
2001
Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre. Incremental Verification by Abstraction. //TACAS 2001: 98-112//
Dawn Song, Sergey Berezin, Adrian Perrig. Athena: a novel approach to efficient automatic security protocol analysis //Special issue of Journal of Computer Security, v. 9:1,2, pp.47-74, 2001.//
- As I found out later, our Athena paper is somewhat unclear about
the fine details of the split rule. The implications are
that this seemingly elementary step might in fact turn out to be
undecidable. Whether there is an algorithm or not became an open
problem, and since none of the authors has time to figure it out, I'm
putting out a short document about the problem in the hope that
someone else will solve it. So, please notify me if you find a
solution.
- Sergey Berezin. Extensions to Athena: Constraint Satisfiability Problem and New Pruning Theorems Based on Type System Extensions for Messages // Unpublished manuscript, 2001.// (Postscript)
2000
Sergey Berezin, Edmund Clarke, Armin Biere, Yunshan Zhu. Verification of OOO Processor Designs Using Model Checking and a Light-Weight Completion Function //In a special issue of FMSD, 2000.//
1999
Sergey Berezin. Combining Model Checking and Theorem Proving; in Harware Verification. //Thesis Proposal, January 27, 1999. An eternal draft.// (Postscript, and related material page)
1998
Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zhu. Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. //CMU TR CMU-CS-98-124, April 20, 1998, and in Proceedings of FMCAD'98 in LNCS 1522. // ( Postscript)
Edmund M. Clarke, Sergey Berezin. Model Checking: Historical Perspective and Example. //Proceedings of Analytic Tableaux and Related Methods, 1998.//
1997
Sergey Berezin, Sergio Campos, Edmund M. Clarke. Compositional Reasoning in Model Checking. //CMU TR CMU-CS-98-106, February 2, 1998, and in Proceeding of COMPOS'97 Workshop, LNCS 1536.// ( Postscript)Sergey Berezin, Dilian Gurov. A Compositional Proof System for the Modal mu-calculus and CCS. //CMU TR CMU-CS-97-105, January 15, 1997.// (Postscript)
1996
Sergey Berezin, Edmund Clarke, Somesh Jha, Will Marrero. Model Checking Algorithms for the mu-Calculus. //CMU TR CMU-CS-96-180, September 1996. In Proof, Language, and Interaction, edited by G. Plotkin, MIT Press, 2000. ISBN: 0262161885// ( Postscript)Dilian Gurov, Sergey Berezin, Bruce M. Kapron. A Modal mu-Calculus and a Proof System for Value Passing Processes. //INFINITY Workshop, Aug. 1996, Pisa, Italy. ENTCS, Volume 5.//
1995
S. Berezin. Hierarchical verification of parallel processes using the modal mu-calculus. ( gzipped Poscript, 462K)//Master thesis. Novosibirsk State University, Novosibirsk, Russia, 1995 (in Russian).//S. Berezin. A Proof System for Non-Classical Verification of Distributed Systems: An Induction on the Number of Parallel Processes.(gzipped Poscript, 95K) //A part of master thesis. Novosibirsk State University, Novosibirsk, Russia, June 1995 (in English).//
1994
S.A. Berezine. Model Checking in mu-calculus for distributed systems. //In Specification, verification, and net models of concurrent systems. Institute of Informatics Systems, Novosibirsk, Russia, 1994.//S.A. Berezin, N.V. Shilov. An Approach to Effective Model-Checking of Real-Time Finite-State Machines in Mu-Calculus. //Proceedings of LFCS'94, in LNCS vol. 813 pp.47-55. St. Petersburg, Russia, July 1994.//