@InProceedings{BarrettBerezin04, author = {Clark Barrett and Sergey Berezin}, title = {{CVC} {L}ite: A New Implementation of the Cooperating Validity Checker}, crossref = {CAV2004}, OPTpages = {}, } @InProceedings{ChangBerezinDill04, author = {Jacob Chang and Sergey Berezin and David L. Dill}, title = {Using Interface Refinement to Integrate Formal Verification into the Design Cycle}, crossref = {CAV2004}, OPTpages = {}, } @proceedings{CAV2004, editor = {Rajeev Alur and Doron A. Peled}, title = {Computer Aided Verification, 16th International Conference, CAV 2004, Boston, Massachusetts, USA, July 13-17, 2004, Proceedings}, booktitle = {CAV}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, OPTvolume = {}, year = {2004}, OPTisbn = {}, } @InProceedings{BBSCGD04, author = {Clark Barrett and Sergey Berezin and Igor Shikanian and Marsha Chechik and Arie Gurfinkel and David L. Dill}, title = {A Practical Approach to Partial Functions in {CVC} {L}ite}, booktitle = {{PDPAR}'04 Workshop, Cork, Ireland}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = jul, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{BBD03, author = {Clark Barrett and Sergey Berezin}, title = {A Proof-Producing Boolean Search Engine}, key = {2003}, booktitle = {{PDPAR}'03 Workshop, Miami, Florida}, OPTpages = {}, year = {2003}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = jul, OPTorganization = {}, OPTpublisher = {}, note = {}, OPTannote = {} } @InProceedings{AbuHaimedBerezinDill03, author = {Husam Abu-Haimed and Sergey Berezin and David L. Dill}, title = {Strengthening Invariants by Symbolic Consistency Testing}, key = {2003}, crossref = {CAV2003}, pages = {407-419}, year = {2003}, } @proceedings{CAV2003, editor = {Warren A. Hunt and Fabio Somenzi}, title = {Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings}, booktitle = {CAV}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2725}, year = {2003}, isbn = {3-540-40524-0}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{BerezinGaneshDill03, author = {Sergey Berezin and Vijay Ganesh and David L. Dill}, title = {An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic}, booktitle = {TACAS'03}, key = {2003}, OPTkey = {}, pages = {521--536}, year = {2003}, editor = {H. Garavel and J. Hatcliff}, volume = {2619}, series = {Lecture Notes in Computer Science}, OPTaddress = {{W}arsaw {P}oland}, month = apr, OPTorganization = {}, publisher = {Springer Verlag}, OPTnote = {to appear}, OPTannote = {} } @TechReport{OmegaInCVC02, author = {Sergey Berezin and Vijay Ganesh and David L. Dill}, title = {Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic}, institution = {Stanford University}, year = {2002}, key = {2002}, OPTkey = {}, OPTtype = {}, OPTnumber = {}, OPTaddress = {}, OPTmonth = nov, OPTnote = {Draft. To appear soon.}, OPTannote = {} } @InProceedings{GaneshBerezinDill02, author = {Vijay Ganesh and Sergey Berezin and David L. Dill}, title = {Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods}, booktitle = {4th International Conference FMCAD'02}, OPTkey = {}, pages = {171--186}, key = {2002}, year = {2002}, editor = {M.D. Aagaard and J.W. O'Leary}, volume = {2517}, OPTnumber = {}, series = {Lecture Notes in Computer Science}, address = {{P}ortland {OR} {USA}}, month = nov, OPTorganization = {}, publisher = {Springer Verlag}, OPTannote = {} } @PhdThesis{BerezinThesis02, author = {Sergey Berezin}, title = {Model Checking and Theorem Proving: a Unified Framework}, school = {Carnegie Mellon University}, year = {2002}, key = {2002}, OPTkey = {}, OPTtype = {}, OPTaddress = {}, month = jan, OPTnote = {}, OPTannote = {} } @Misc{sympURL, author = {Sergey Berezin}, title = {The {SyMP} tool}, year = "2001", key = {2001}, howpublished = "\texttt{http:// www.cs.cmu.edu /}\verb+~+\texttt{modelcheck/ symp.html}", } @inproceedings{ berezin98combining, author = "Sergey Berezin and Armin Biere and Edmund M. Clarke and Yunshan Zhu", title = "Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification", booktitle = "Formal Methods in Computer-Aided Design, {FMCAD}'98", pages = "369-386", key = {1998}, year = "1998", number={1522}, series={Lecture Notes in Computer Science}, publisher={Springer-Verlag}, url = "citeseer.nj.nec.com/berezin98combining.html" } @article{athena2000, title = {Athena: a novel approach to efficient automatic security protocol analysis}, key = {2000}, author = {Dawn Song and Sergey Berezin and Adrian Perrig}, journal = "Journal of Computer Security", volume = 9, issue = "1,2", pages = {47--74}, year = {2001}, } @inproceedings{compos97, author={Sergey Berezin and Sergio Campos and Edmund M. Clarke}, title ={Compositional Reasoning in Model Checking}, booktitle={COMPOS'97}, key = {1997}, series = "LNCS", volume = 1536, publisher={Springer-Verlag}, year={1997}, month=sep, } @InProceedings{tacas2001, author = {Yassine Lakhnech and Saddek Bensalem and Sergey Berezin and Sam Owre}, title = {Incremental Verification by Abstraction}, key = {2001}, pages = {98--112}, editor = {Tiziana Margaria and Wang Yi}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS'01, Genova, Italy, April 2-6, 2001}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2031}, year = {2001}, isbn = {3-540-41865-2}, } @Article{FMSD2000, author = {Sergey Berezin and Edmund Clarke and Armin Biere and Yunshan Zhu}, title = {Verification of {OOO} Processor Designs Using Model Checking and a Light-Weight Completion Function}, journal = {FMSD}, year = {2000}, key = {2000}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {To appear}, OPTannote = {} } @InProceedings{HistoricalPerspective98, author = {Edmund M. Clarke and Sergey Berezin}, title = {Model Checking: Historical Perspective and Example}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, {TABLEAUX}'98}, year = {1998}, key = {1998}, editor = {Harrie de Swart}, pages = {18--24}, volume = {1397}, OPTnumber = {}, series = {Lecture Notes in Computer Science}, OPTaddress = {}, month = may, OPTorganization = {}, publisher = {Springer Verlag}, } @InProceedings{Berezin:LFSC94, author = {Sergey Berezin and Nikolay V. Shilov}, title = {An Approach to Effective Model-Checking of Real-Time Finite-State Machines in Mu-Calculus}, pages = {47--55}, booktitle = {Logical Foundations of Computer Science, Third International Symposium, {LFCS}'94}, year = {1994}, key = {1994}, editor = {Anil Nerode and Yuri Matiyasevich}, volume = {813}, series = {Lecture Notes in Computer Science}, month = jul, publisher = {Springer Verlag}, } @TechReport{CPS:TR97, author = {Sergey Berezin and Dilian Gurov}, title = {A Compositional Proof System for the Modal mu-calculus and CCS}, institution = {Carnegie Mellon University}, year = {1997}, key = {1997}, OPTkey = {}, OPTtype = {}, number = {CMU-CS-97-105}, OPTaddress = {}, month = jan, OPTnote = {}, OPTannote = {} } @InProceedings{VPP:INFINITY96, author = {Dilian Gurov and Sergey Berezin and Bruce M. Kapron}, title = {A Modal mu-Calculus and a Proof System for Value Passing Processes}, booktitle = {INFINITY Workshop}, OPTkey = {}, OPTpages = {}, year = {1996}, key = {1996}, OPTeditor = {}, volume = {5}, OPTnumber = {}, series = {ENTCS}, OPTaddress = {}, month = aug, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @MastersThesis{master:thesis95, author = {S. Berezin}, title = {Hierarchical verification of parallel processes using the modal mu-calculus}, school = {Novosibirsk State University}, year = {1995}, key = {1995}, OPTkey = {}, OPTtype = {}, OPTaddress = {}, OPTmonth = {}, note = {in Russian}, OPTannote = {} } @TechReport{Berezin:muCalc:TR96, author = {Sergey Berezin and Edmund Clarke and Somesh Jha and Will Marrero}, title = {Model Checking Algorithms for the mu-Calculus}, institution = {Cargegie Mellon University}, year = {1996}, key = {1996}, OPTkey = {}, OPTtype = {}, number = {CMU-CS-96-180}, OPTaddress = {}, month = sep, note = {Also published as \cite{Berezin:muCalc00}}, OPTannote = {} } @InCollection{Berezin:muCalc00, author = {Sergey Berezin and Edmund Clarke and Somesh Jha and Will Marrero}, title = {Model Checking Algorithms for the mu-Calculus}, booktitle = {Proof, Language, and Interaction}, OPTkey = {}, OPTpages = {}, publisher = {MIT Press}, year = {2000}, key = {2000}, editor = {G. Plotkin and Colin P. Stirling and Mads Tofte and R. Milner}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTtype = {}, OPTchapter = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InCollection{Berezine94, author = {S.A. Berezine}, title = {Model Checking in mu-calculus for distributed systems}, publisher = {Institute of Informatics Systems, Novosibirsk, Russia}, year = {1994}, key = {1994}, booktitle = {Specification, verification, and net models of concurrent systems}, } @InCollection{BerezinShilovShneider93, author = {S.A. Berezin and N.V. Shilov and P.V. Shneider}, title = {An effective model checking for Mu-calculus: from finite systems towards systems with real time}, booktitle = {Bulletin of Novosibirsk Computing Center}, OPTkey = {}, key = {1993}, OPTpages = {}, OPTpublisher = {}, year = {1993}, OPTeditor = {}, OPTvolume = {}, number = {1}, series = {Computer Science}, OPTtype = {}, OPTchapter = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} }