% This file was created with JabRef 2.5. % Encoding: UTF8 @STRING{LICS04 = {LICS'04: Proceedings of the 19th IEEE Symposium on Logic in Computer Science}} @STRING{LNCS = {}} @INPROCEEDINGS{aagaard03hazards, author = {M.~Aagaard}, title = {A {H}azards-{B}ased {C}orrectness {S}tatement for {P}ipelined {C}ircuits.}, booktitle = {Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference}, year = {2003}, pages = {66-80}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/charme/2003}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2860{\&}spage=66}, file = {aagard.pdf:/dsk/l1/misc/doc/verif_archi/aagard.pdf:PDF}, keywords = {pipeline} } @INPROCEEDINGS{alder06ticc, author = {B.T.~Adler and L.~de Alfaro and L.~Dias da Silva and M.~Faella and A.~Legay and V.~Raman and P.~Roy}, title = {Ticc: {A T}ool for {I}nterface {C}ompatibility and {C}omposition.}, booktitle = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification}, year = {2006}, pages = {59-62}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2006}, ee = {http://dx.doi.org/10.1007/11817963_8}, file = {tiicctool.pdf:/dsk/l1/misc/doc/interface/tiicctool.pdf:PDF}, keywords = {interface, wrapper} } @INPROCEEDINGS{DBLP:conf/frocos/AlfaroSFLRS05, author = {Luca de Alfaro and Leandro Dias da Silva and Marco Faella and Axel Legay and Pritam Roy and Maria Sorea}, title = {{Sociable Interfaces.}}, booktitle = {FroCos'05: Proceedings of the 5th International Workshop on Frontiers of Combining Systems}, year = {2005}, pages = {81-105}, address = {Vienna, Austria}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/frocos/2005}, ee = {http://dx.doi.org/10.1007/11559306_5} } @INPROCEEDINGS{alur98alternatingtime, author = {Rajeev Alur and Thomas A. Henzinger and Orna Kupferman}, title = {{Alternating-Time Temporal Logic}}, booktitle = {COMPOS}, year = {1997}, pages = {23-60}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/compos/1997}, ee = {http://link.springer.de/link/service/series/0558/bibs/1536/15360023.htm}, keywords = {atl} } @INPROCEEDINGS{DBLP:conf/lpar/AndrausLS08, author = {Zaher S. Andraus and Mark H. Liffiton and Karem A. Sakallah}, title = {Reveal: A Formal Verification Tool for Verilog Designs}, booktitle = {LPAR}, year = {2008}, pages = {343-352}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/lpar/2008}, ee = {http://dx.doi.org/10.1007/978-3-540-89439-1_25}, keywords = {CEGAR,Hardware, TOOLS} } @INPROCEEDINGS{DBLP:conf/dac/AndrausS04, author = {Zaher S. Andraus and Karem A. Sakallah}, title = {Automatic abstraction and verification of verilog models}, booktitle = {DAC}, year = {2004}, pages = {218-223}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/dac/2004}, ee = {http://doi.acm.org/10.1145/996566.996629}, file = {:Abstraction/Andraus_DAC_Vapor.pdf:PDF}, keywords = {Abstraction, Hardware, Verilog, TOOLS, Vapor} } @INPROCEEDINGS{Awhed04Proving, author = {M.~Awedh and F.~Somenzi}, title = {Proving More Properties with Bounded Model Checking}, booktitle = {CAV'04: Proceedings of the 16th International Conference on Computer Aided Verification}, year = {2004}, pages = {96-108}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2004}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=96}, file = {:BMC/ProvingMorePropwithBC04.pdf:PDF}, keywords = {BMC, VIS} } @INPROCEEDINGS{bmethod99meteor, author = {P.~Behm and P.~Benoit and A.~Faivre and J-M.~Meynadier}, title = {{M{\'e}t{\'e}or: A Successful Application of B in a Large Project}}, booktitle = {World Congress on Formal Methods}, year = {1999}, pages = {369-387}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/fm/1999-1}, ee = {http://link.springer.de/link/service/series/0558/bibs/1708/17080369.htm} } @INPROCEEDINGS{DBLP:conf/vmcai/Bradley11, author = {Aaron R. Bradley}, title = {SAT-Based Model Checking without Unrolling}, booktitle = {VMCAI}, year = {2011}, pages = {70-87}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/vmcai/2011}, ee = {http://dx.doi.org/10.1007/978-3-642-18275-4_7} } @INPROCEEDINGS{bruns00generalized, author = {G.~Bruns and P.~Godefroid}, title = {{Generalized Model Checking: Reasoning about Partial State Spaces}}, booktitle = {CONCUR'2000: Proceedings of the 11th International Conference on Concurrency Theory}, year = {2000}, editor = {Nicolas Halbwachs and Doron Peled}, series = {Lecture Notes in Computer Science}, pages = {168-182}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/concur/2000}, ee = {http://link.springer.de/link/service/series/0558/bibs/1877/18770168.htm}, file = {godefroid00.pdf:/dsk/l1/misc/doc/abstraction/godefroid00.pdf:PDF}, keywords = {3-valued, Kripke structure, abstraction} } @INPROCEEDINGS{burns99partial, author = {G.~Bruns and P.~Godefroid}, title = {{Model Checking Partial State Spaces with 3-Valued Temporal Logics}}, booktitle = {CAV'99: Proceedings of the 11th conference on Computer Aided Verification}, year = {1999}, series = {Lecture Notes in Computer Science}, pages = {274-287}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/1999}, ee = {http://link.springer.de/link/service/series/0558/bibs/1633/16330274.htm}, file = {burns99partial.pdf:/dsk/l1/misc/doc/abstraction/burns99partial.pdf:PDF}, keywords = {tree automata, CTL, automata approach}, owner = {cecile}, timestamp = {2006.04.25} } @INPROCEEDINGS{Buttner05isformal, author = {W. B{\"u}ttner}, title = {{Is Formal Verification Bound to Remain a Junior Partner of Simulation?}}, booktitle = {CHARME'2005: Proceedings of the Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference}, year = {2005}, editor = {Dominique Borrione, Wolfgang J. Paul}, volume = {3725}, series = {Lecture Notes in Computer Science}, pages = {1}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/charme/2005}, ee = {http://dx.doi.org/10.1007/11560548_1}, owner = {cecile}, timestamp = {2006.06.27} } @INPROCEEDINGS{DBLP:conf/fmcad/ChauhanCKSVW02, author = {P.~Chauhan and E.M.~Clarke and J.H.~Kukula and S.~Sapra and H.~Veith and D.~Wang}, title = {Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis}, booktitle = {FMCAD'02: Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design }, year = {2002}, pages = {33-51}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/fmcad/2002}, ee = {http://link.springer.de/link/service/series/0558/bibs/2517/25170033.htm}, file = {:Cegar/AutomatedAbstractionRefinment02Chauchan.pdf:PDF}, keywords = {Cegar, SAT} } @INPROCEEDINGS{chechik05framework, author = {Marsha Chechik and Arie Gurfinkel}, title = {A Framework for Counterexample Generation and Exploration.}, booktitle = {FASE}, year = {2005}, pages = {220-236}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/fase/2005}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3442{\&}spage=220}, file = {chechik05a.pdf:/dsk/l1/misc/doc/abstraction/chechik05a.pdf:PDF} } @INPROCEEDINGS{ChocklerKV01, author = {H.~Chockler and O.~Kupferman and M.Y.~Vardi}, title = {Coverage Metrics for Temporal Logic Model Checking}, booktitle = {TACAS'01: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2001}, series = {LNCS}, pages = {528-542}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/2001}, ee = {http://link.springer.de/link/service/series/0558/bibs/2031/20310528.htm}, file = {:Fault/Coverage_Metric_for_temporal_MC01.pdf:PDF}, keywords = {coverage} } @INPROCEEDINGS{DBLP:conf/fmcad/CimattiDJR09, author = {Alessandro Cimatti and Jori Dubrovin and Tommi A. Junttila and Marco Roveri}, title = {Structure-aware computation of predicate abstraction}, booktitle = {FMCAD}, year = {2009}, pages = {9-16}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/fmcad/2009}, ee = {http://dx.doi.org/10.1109/FMCAD.2009.5351149}, file = {:Cegar/StructureAwareComputationofPredicateAbstraction09.pdf:PDF}, keywords = {Abstraction} } @INPROCEEDINGS{DBLP:conf/sfm/ClaessenR06, author = {Koen Claessen and Jan-Willem Roorda}, title = {An Introduction to Symbolic Trajectory Evaluation}, booktitle = {SFM}, year = {2006}, pages = {56-77}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/sfm/2006}, ee = {http://dx.doi.org/10.1007/11757283_3} } @INPROCEEDINGS{clarke03cegar, author = {E.M.~Clarke}, title = {Counterexample-Guided Abstraction Refinement}, booktitle = {TIME}, year = {2003}, pages = {7}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/time/2003}, ee = {http://csdl.computer.org/comp/proceedings/time-ictl/2003/1912/00/19120007.pdf}, file = {ce03time.pdf:/dsk/l1/misc/doc/CEGAR/ce03time.pdf:PDF}, keywords = {abstraction, CEGAR} } @INPROCEEDINGS{clarkeE81design, author = {E.M.~Clarke and E.A.~Emerson}, title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.}, booktitle = {Logic of Programs}, year = {1981}, pages = {52-71}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/lop/1981} } @INPROCEEDINGS{ClarkeGJLV00, author = {E.M.~Clarke and O.Grumberg and S.~Jha and Y.~Lu and H.~Veith}, title = {{Counterexample-Guided Abstraction Refinement.}}, booktitle = {CAV'00: Proceedings of the 12th International Conference on Computer Aided Verification}, year = {2000}, pages = {154-169}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2000} } @INPROCEEDINGS{DBLP:conf/birthday/ClarkeKV10, author = {Edmund M. Clarke and Robert P. Kurshan and Helmut Veith}, title = {The Localization Reduction and Counterexample-Guided Abstraction Refinement}, booktitle = {Essays in Memory of Amir Pnueli}, year = {2010}, pages = {61-71}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/birthday/2010pnueli}, ee = {http://dx.doi.org/10.1007/978-3-642-13754-9_4} } @INPROCEEDINGS{DBLP:conf/lics/ClarkeLM89, author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan}, title = {Compositional Model Checking}, booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science}, year = {1989}, pages = {353-362}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/lics/LICS4}, file = {clarke89compo.ps:/dsk/l1/misc/doc/model_check/clarke89compo.ps:PDF}, keywords = {composition, model checking, Kripke structure, Moore machine, CTL} } @INPROCEEDINGS{DBLP:conf/sat/ClarkeTVW03, author = {Edmund M. Clarke and Muralidhar Talupur and Helmut Veith and Dong Wang}, title = {SAT Based Predicate Abstraction for Hardware Verification}, booktitle = {SAT}, year = {2003}, pages = {78-92}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/sat/2003}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2919{\&}spage=78}, file = {:Abstraction/SATBasedPredicateAbstactforHWVerif2004.pdf:PDF}, keywords = {SAT, predicate abstraction, hardware} } @INPROCEEDINGS{CouvreurEPPW02, author = {J-M.~Couvreur and E.~Encrenaz and E.~Paviot-Adet and D.~Poitrenaud and P-A.~Wacrenier}, title = {Data Decision Diagrams for Petri Net Analysis.}, booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets}, year = {2002}, pages = {101-120}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/apn/2002}, ee = {http://link.springer.de/link/service/series/0558/bibs/2360/23600101.htm} } @INPROCEEDINGS{couvreur05hierarchie, author = {J-M.~Couvreur and Y.~Thierry-Mieg}, title = {{Hierarchical Decision Diagrams to Exploit Model Structure.}}, booktitle = {FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems}, year = {2005}, editor = {Farn Wang}, volume = {3731}, series = {Lecture Notes in Computer Science}, pages = {443-457}, address = {Taipei, Taiwan}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/forte/2005}, ee = {http://dx.doi.org/10.1007/11562436_32} } @INPROCEEDINGS{DBLP:conf/vmcai/DamsN05, author = {D.~Dams and K.~S.~Namjoshi}, title = {{Automata as Abstractions.}}, booktitle = {VMCAI'05: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation}, year = {2005}, series = {Lecture Notes in Computer science}, pages = {216-232}, address = {Paris, France}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/vmcai/2005}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3385{\&}spage=216}, file = {automata_aabstr.pdf:/dsk/l1/misc/doc/modular/abstraction/automata_aabstr.pdf:PDF}, keywords = {tree automata, CTL, automata approach} } @INPROCEEDINGS{DBLP:conf/lics/DamsN04, author = {D.~Dams and K.~S.~Namjoshi}, title = {The Existence of Finite Abstractions for Branching Time Model Checking.}, booktitle = {LICS04}, year = {2004}, pages = {335-344}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/lics/2004}, ee = {http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920335abs.htm}, file = {abstractforbtl.pdf:/dsk/l1/misc/doc/ctl_auto/abstractforbtl.pdf:PDF}, keywords = {CTL, tree automata ,model checking, automata approach} } @INPROCEEDINGS{DBLP:conf/icse/DwyerHJLPRZV01, author = {Matthew B. Dwyer and John Hatcliff and Roby Joehanes and Shawn Laubach and Corina S. Pasareanu and Robby and Hongjun Zheng and Willem Visser}, title = {Tool-Supported Program Abstraction for Finite-State Verification.}, booktitle = {ICSE}, year = {2001}, pages = {177-187}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/icse/2001}, file = {bandera.pdf:/dsk/l1/misc/doc/softMC/bandera.pdf:PDF}, keywords = {software, model-checking, CEGAR} } @INPROCEEDINGS{DBLP:conf/icse/EasterbrookCDGLPTT03, author = {S.M.~Easterbrook and M.~Chechik and B.~Devereux and A.~Gurfinkel and A.~Lai and V.~Petrovykh and A.~Tafliovich and C.~Thompson-Walsh}, title = {{$\chi$Chek: A Model Checker for Multi-Valued Reasoning.}}, booktitle = {ICSE'03: Proceedings of the 25th International Conference on Software Engineering}, year = {2003}, pages = {804-805}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/icse/2003}, ee = {http://computer.org/proceedings/icse/1877/18770804.pdf} } @INPROCEEDINGS{EasterbrookC01, author = {Steve M. Easterbrook and Marsha Chechik}, title = {A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints.}, booktitle = {ICSE}, year = {2001}, pages = {411-420}, bibsource = {DBLP,http://dblp.uni-trier.de}, crossref = {DBLP:conf/icse/2001}, file = {easterbrook01a.pdf:/dsk/l1/misc/doc/multi_valued/easterbrook01a.pdf:PDF}, keywords = {abstraction, 3-valued, 4-valued, logic, model checking} } @INPROCEEDINGS{emerson82desision, author = {E.A.~Emerson and J.Y.~Halpern}, title = {Decision Procedures and Expressiveness in the Temporal Logic of Branching Time}, booktitle = {STOC}, year = {1982}, pages = {169-180}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/stoc/STOC14}, file = {ctl_emerson82.pdf:/dsk/l1/misc/doc/model_check/ctl_emerson82.pdf:PDF}, keywords = {CTL, model checking} } @INPROCEEDINGS{DBLP:conf/date/GanaiGA05, author = {Malay K. Ganai and Aarti Gupta and Pranav Ashar}, title = {Verification of Embedded Memory Systems using Efficient Memory Modeling}, booktitle = {DATE}, year = {2005}, pages = {1096-1101}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/date/2005}, ee = {http://doi.ieeecomputersociety.org/10.1109/DATE.2005.325}, file = {:Abstraction/VerifEmbededMemoryusingEMM09.pdf:PDF}, keywords = {Abstraction, Memory,}, owner = {cecile}, timestamp = {2010.06.10} } @INPROCEEDINGS{DBLP:conf/cav/GodefroidJ02, author = {P.~Godefroid and R.~Jagadeesan}, title = {Automatic Abstraction Using Generalized Model Checking.}, booktitle = {CAV}, year = {2002}, pages = {137-150}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2002}, ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm}, keywords = {Abstraction} } @INPROCEEDINGS{GrafS97pvs, author = {S.~Graf and H.~Sa\"{\i}di}, title = {{Construction of Abstract State Graphs with PVS.}}, booktitle = {CAV}, year = {1997}, pages = {72-83}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/1997}, file = {graf97cinstructionpvs.ps:/dsk/l1/misc/doc/abstraction/graf97cinstructionpvs.ps:PDF}, keywords = {abstraction, CEGAR} } @INPROCEEDINGS{grumberg05abstraction, author = {Orna Grumberg}, title = {{Abstraction and Refinement in Model Checking.}}, booktitle = {FMCO'05: 4th International Symposium on Formal Methods for Components and Objects,}, year = {2005}, pages = {219-242}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/fmco/2005}, ee = {http://dx.doi.org/10.1007/11804192_11}, keywords = {abstraction, refinement, CEGAR} } @INPROCEEDINGS{DBLP:conf/sfm/GuptaGW06, author = {Aarti Gupta and Malay K. Ganai and Chao Wang}, title = {SAT-Based Verification Methods and Applications in Hardware Verification}, booktitle = {SFM}, year = {2006}, pages = {108-143}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/sfm/2006}, ee = {http://dx.doi.org/10.1007/11757283_5}, file = {:BMC/SATBasedVerifMethodAndApplitoHdw2006.pdf:PDF}, keywords = {SAT, verification,} } @INPROCEEDINGS{gurfinkelC06waste, author = {A.~Gurfinkel and M.~Chechik}, title = {{Why Waste a Perfectly Good Abstraction?.}}, booktitle = {T{ACAS}'06: {P}roceedings of the 12th international conference on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of {S}ystems}, year = {2006}, series = {Lecture Notes in Computer Science}, pages = {212-226}, address = {Vienna, Austria}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/2006}, ee = {http://dx.doi.org/10.1007/11691372_14}, file = {gurfinkel_tacas_06.pdf:/dsk/l1/misc/doc/abstraction/gurfinkel_tacas_06.pdf:PDF}, keywords = {abstraction, 3-valued, 4-valued, logic, model checking} } @INPROCEEDINGS{DBLP:conf/vmcai/GurfinkelWC06, author = {Arie Gurfinkel and Ou Wei and Marsha Chechik}, title = {Systematic Construction of Abstractions for Model-Checking}, booktitle = {VMCAI}, year = {2006}, pages = {381-397}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/vmcai/2006}, ee = {http://dx.doi.org/10.1007/11609773_25} } @INPROCEEDINGS{GurfinkelWC06, author = {Gurfinkel, A. and Wei, O. and Chechik, M.}, title = {Systematic {C}onstruction of {A}bstractions for {M}odel-{C}hecking.}, booktitle = {V{MCAI}'06: {P}roceedings of the 7th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation}, year = {2006}, pages = {381-397}, address = {Charleston, USA}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/vmcai/2006}, ee = {http://dx.doi.org/10.1007/11609773_25}, keywords = {abstraction, abstract interpretation} } @INPROCEEDINGS{JainKSC05, author = {Jain, H. and Kroening, D. and Sharygina, N. and Clarke, E.M.}, title = {Word {L}evel {P}redicate {A}bstraction and {R}efinement for {V}erifying {RTL} {V}erilog.}, booktitle = {D{AC}'05: {P}roceedings of the 42nd {D}esign {A}utomation {C}onference}, year = {2005}, editor = {William H. Joyner Jr., Grant Martin, Andrew B. Kahng}, series = {ACM}, pages = {445-450}, address = {San Diego, USA}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/dac/2005}, ee = {http://doi.acm.org/10.1145/1065579.1065697} } @INPROCEEDINGS{jhala01microarchi, author = {Jhala, R. and McMillan, K.L.}, title = {Microarchitecture {V}erification by {C}ompositional {M}odel {C}hecking.}, booktitle = {C{AV}'01: {P}roceedings of the 13th {I}nternational {C}onference on {C}omputer {A}ided {V}erification}, year = {2001}, editor = {G\'erard Berry, Hubert Comon, Alain Finkel}, series = {Lecture Notes in Computer Science}, pages = {396-410}, address = {Paris, France}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2001}, ee = {http://link.springer.de/link/service/series/0558/bibs/2102/21020396.htm} } @INPROCEEDINGS{Somenzi04Circuscav, author = {HoonSang Jin and Mohammad Awedh and Fabio Somenzi}, title = {CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking}, booktitle = {CAV'04: Proceedings of the 16th International Conference onComputer Aided Verification }, year = {2004}, pages = {519-522}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2004}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=519}, file = {:SAT/CirCUsToward.pdf:PDF}, keywords = {SAT, SAT solver, VIS} } @INPROCEEDINGS{DBLP:conf/tacas/JinHS05, author = {HoonSang Jin and HyoJung Han and Fabio Somenzi}, title = {Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit}, booktitle = {TACAS'05: Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2005}, pages = {287-300}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/2005}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3440{\&}spage=287}, file = {:SAT/efficientConflict05Jin.pdf:PDF}, keywords = {SAT, All-sat} } @INPROCEEDINGS{somenzi04Circus, author = {H*.~Jin and F.~Somenzi}, title = {CirCUs: A Hybrid Satisfiability Solver}, booktitle = {SAT'04: The 7th International Conference on Theory and Applications of Satisfiability Testing}, year = {2004}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/sat/2004}, ee = {http://www.satisfiability.org/SAT04/programme/24.pdf}, owner = {cecile}, timestamp = {2009.01.27} } @INPROCEEDINGS{larsen88modal, author = {K.~G.~Larsen and B.~Thomsen}, title = {A {M}odal {P}rocess {L}ogic}, booktitle = {Third Annual Symposium on Logic in Computer Science}, year = {1988}, pages = {203-210}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/lics/LICS3} } @INPROCEEDINGS{DBLP:conf/iccad/ManoliosSV06, author = {Panagiotis Manolios and Sudarshan K. Srinivasan and Daron Vroon}, title = {Automatic memory reductions for RTL model verification}, booktitle = {ICCAD}, year = {2006}, pages = {786-793}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/iccad/2006}, ee = {http://doi.acm.org/10.1145/1233501.1233663}, file = {:Abstraction/AutomaticMemoryReductionforRTL06.pdf:PDF}, keywords = {Abstraction, memory} } @INPROCEEDINGS{mcmillan98tomasulo, author = {K.L.~McMillan}, title = {Verification of an {I}mplementation of {T}omasulo's {A}lgorithm by {C}ompositional {M}odel {C}hecking.}, booktitle = {C{AV}'98: {P}roceddings of the 10th {I}nternational {C}onference on {C}omputer {A}ided {V}erification}, year = {1998}, editor = {Alan J. Hu, Moshe Y. Vardi}, volume = {1427}, series = {Lecture Notes in Computer Science}, pages = {110-121}, address = {Vancouver, Canada}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/1998} } @INPROCEEDINGS{mcmillan02applyingSat, author = {Kenneth L. McMillan}, title = {Applying SAT Methods in Unbounded Symbolic Model Checking}, booktitle = {CAV'02: Proceedings of the 14th International Conference on Computer Aided vVrification}, year = {2002}, pages = {250-264}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2002}, ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040250.htm}, file = {:BMC/Mcmillan02applyingSat.pdf:PDF} } @INPROCEEDINGS{DBLP:conf/cav/McMillan97, author = {Kenneth L. McMillan}, title = {{A Compositional Rule for Hardware Design Refinement.}}, booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification}, year = {1997}, volume = {1254}, series = {Lecture Notes in Computer Science}, pages = {24-35}, adress = {Haifa, Israel}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/1997} } @INPROCEEDINGS{Morin-AlloryB06, author = {K.~Morin-Allory and D.~Borrione}, title = {Proven {C}orrect {M}onitors from {PSL} {S}pecifications.}, booktitle = {D{ATE}'06: {P}roceedings of the {C}onference on {D}esign, {A}utomation and {T}est in {E}urope}, year = {2006}, editor = {{Georges G. E. Gielen}}, pages = {1246-1251}, address = {Munich, Germany}, organization = {European Design and Automation Association}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/date/2006p}, ee = {http://doi.acm.org/10.1145/1131827} } @INPROCEEDINGS{DBLP:conf/dac/MoskewiczMZZM01, author = {M.W.~Moskewicz and C.F.~Madigan and Y.~Zhao and L.~Zhang and S.~Malik}, title = {Chaff: Engineering an Efficient SAT Solver}, booktitle = {DAC'01: Proceedings of the 38th Design Automation Conference}, year = {2001}, pages = {530-535}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/dac/2001}, ee = {http://jamaica.ee.pitt.edu/Archives/ProceedingArchives/Dac/Dac2001/papers/2001/dac01/pdffiles/33_1.pdf}, file = {:SAT/4 - moskewicz01chaff.pdf:PDF} } @INPROCEEDINGS{DBLP:conf/sbmf/MouraB09, author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner}, title = {Satisfiability Modulo Theories: An Appetizer}, booktitle = {SBMF}, year = {2009}, pages = {23-36}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/sbmf/2009}, ee = {http://dx.doi.org/10.1007/978-3-642-10452-7_3} } @INPROCEEDINGS{DBLP:conf/tacas/MouraB08, author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner}, title = {Z3: An Efficient SMT Solver}, booktitle = {TACAS}, year = {2008}, pages = {337-340}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/2008}, ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_24} } @INPROCEEDINGS{DBLP:conf/cav/Namjoshi03, author = {Kedar S. Namjoshi}, title = {Abstraction for Branching Time Properties.}, booktitle = {CAV}, year = {2003}, pages = {288-300}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2003}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=288}, file = {abstractforbtl.pdf:/dsk/l1/misc/doc/ctl_auto/abstractforbtl.pdf:PDF}, keywords = {abstraction} } @INPROCEEDINGS{DBLP:conf/date/NanshiS08, author = {K.~Nanshi and F.~Somenzi}, title = {Improved Visibility in One-to-Many Trace Concretization}, booktitle = {DATE}, year = {2008}, pages = {819-824}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/date/2008}, ee = {http://dx.doi.org/10.1109/DATE.2008.4484775} } @INPROCEEDINGS{DBLP:conf/dac/NanshiS06, author = {K.~Nanshi and F.~Somenzi}, title = {Guiding simulation with increasingly refined abstract traces}, booktitle = {DAC}, year = {2006}, pages = {737-742}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/dac/2006}, ee = {http://doi.acm.org/10.1145/1146909.1147097} } @INPROCEEDINGS{nejati05stutering, author = {Shiva Nejati and Arie Gurfinkel and Marsha Chechik}, title = {Stuttering Abstraction for Model Checking}, booktitle = {SEFM}, year = {2005}, pages = {311-320}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/sefm/2005}, ee = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.44}, file = {nejati05.pdf:/dsk/l1/misc/doc/abstraction/nejati05.pdf:PDF} } @INPROCEEDINGS{DBLP:conf/tcs/Park81, author = {D.~Park}, title = {{Concurrency and Automata on Infinite Sequences.}}, booktitle = {Proceedings of the 5th GI-Conference on Theoretical Computer Science}, year = {1981}, pages = {167-183}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tcs/1981} } @INPROCEEDINGS{peng02tableau, author = {H.~Peng and Y.~Mokhtari and S.~Tahar}, title = {Environment {S}ynthesis for {C}ompositional {M}odel {C}hecking.}, booktitle = {I{CCD}'02: {P}roceedings of the 20th {I}nternational {C}onference on {C}omputer {D}esign}, year = {2002}, pages = {70-}, address = {Freiburg, Germany}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/iccd/2002}, ee = {http://csdl.computer.org/comp/proceedings/iccd/2002/1700/00/17000070abs.htm} } @INPROCEEDINGS{RaviS04MinimalAssig, author = {K.~Ravi and F.~Somenzi}, title = {Minimal Assignments for Bounded Model Checking}, booktitle = {TACAS'04: Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2004}, series = {LNCS}, pages = {31-45}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/2004}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=31}, file = {:SAT/minimal_assignment_for_bmc.pdf:PDF} } @INPROCEEDINGS{DBLP:conf/cav/RoordaC06, author = {Jan-Willem Roorda and Koen Claessen}, title = {SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation}, booktitle = {CAV}, year = {2006}, pages = {175-189}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2006}, ee = {http://dx.doi.org/10.1007/11817963_19} } @INPROCEEDINGS{roux03ctl, author = {C.~Roux and E.~Encrenaz}, title = {CTL May Be Ambiguous When Model Checking Moore Machines.}, booktitle = {CHARME}, year = {2003}, pages = {164-169}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/charme/2003}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2860{\&}spage=164}, file = {rouxctl.pdf:/dsk/l1/misc/doc/modular/model_checking/rouxctl.pdf:PDF}, keywords = {CTL}, owner = {cecile}, timestamp = {2006.02.28}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2860&spage=164} } @INPROCEEDINGS{DBLP:conf/date/RoychoudhuryMK03, author = {Abhik Roychoudhury and Tulika Mitra and S. R. Karri}, title = {Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol.}, booktitle = {DATE}, year = {2003}, pages = {10828-10833}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/date/2003}, ee = {http://csdl.computer.org/comp/proceedings/date/2003/1870/01/187010828abs.htm}, keywords = {AMBA} } @INPROCEEDINGS{shohamG04monotonic, author = {S.~Shoham and O.~Grumberg}, title = {Monotonic {A}bstraction-{R}efinement for {CTL}.}, booktitle = {T{ACAS}'04: {P}roceedings of the 10th {I}nternational {C}onference on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of {S}ystems}, year = {2004}, editor = {Kurt Jensen, Andreas Podelski}, volume = {2988}, series = {Lecture Notes in Computer Science}, pages = {546-560}, address = {Barcelona, Spain}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/2004}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=546}, file = {monotone-abs-ref.ps:/dsk/l1/misc/doc/ctl_auto/monotone-abs-ref.ps:PDF}, keywords = {CTL , abstraction , 3-valued , refinment loop} } @INPROCEEDINGS{somenzi00efficient, author = {F.~Somenzi and R.~Bloem}, title = {Efficient B{\"u}chi Automata from LTL Formulae.}, booktitle = {CAV}, year = {2000}, pages = {248-263}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/cav/2000}, file = {wring.ps:/dsk/l1/misc/doc/ltl_auto/wring.ps:PDF}, keywords = {LTL, automata approach,}, owner = {cecile}, timestamp = {2006.02.13} } @INPROCEEDINGS{StaberFBD06, author = {Stefan Staber and G{\"o}rschwin Fey and Roderick Bloem and Rolf Drechsler}, title = {Automatic Fault Localization for Property Checking}, booktitle = {Haifa Verification Conference}, year = {2006}, pages = {50-64}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/hvc/2006}, ee = {http://dx.doi.org/10.1007/978-3-540-70889-6_4}, file = {:Debug/FaultLocalizationforpropertychecking-CAD06.pdf:PDF}, keywords = {Debug, SAT} } @INPROCEEDINGS{DBLP:conf/date/SulflowFBKD09, author = {Andr{\'e} S{\"u}lflow and G{\"o}rschwin Fey and C{\'e}cile Braunstein and Ulrich K{\"u}hne and Rolf Drechsler}, title = {Increasing the accuracy of SAT-based debugging}, booktitle = {DATE}, year = {2009}, pages = {1326-1331}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/date/2009}, ee = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=5090609{\&}arnumber=5090870{\&}count=326{\&}index=256}, file = {:Debug/increasingaccuracy-DATE09.pdf:PDF}, keywords = {Debug, SAT, localization reduction, abstraction} } @INPROCEEDINGS{DBLP:conf/tacas/VelevB98, author = {Miroslav N. Velev and Randal E. Bryant}, title = {Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation}, booktitle = {TACAS}, year = {1998}, pages = {136-150}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {DBLP:conf/tacas/1998}, ee = {http://link.springer.de/link/service/series/0558/bibs/1384/13840136.htm}, file = {:Abstraction/EfficientModelingMemoryArraySymbolicTernarySimulation98.pdf:PDF}, keywords = {Abstraction, Memory, STE} } @PROCEEDINGS{DBLP:conf/charme/2003, title = {Correct Hardware Design and Verification Methods CHARME 2003}, year = {2003}, editor = {Daniel Geist and Enrico Tronci}, volume = {2860}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, crossref = {DBLP:conf/charme/2003}, owner = {cecile}, timestamp = {2006.02.02} } @MANUAL{rulebase06userguide, title = {RuleBase Parallel Edition,User's Guide}, author = {Model Checking Systems group}, organization = {IBM Labs}, address = {Haifa, Israel}, year = {2005}, note = {verion 1.26}, owner = {cecile}, timestamp = {2007.03.07} } @INPROCEEDINGS{Vis, author = {The {VIS} group}, title = {{VIS} : {A} {S}ystem for {V}erification and {S}ynthesis}, booktitle = {CAV'96: Proceedings of the 8th International Conference on Computer Aided Verification}, year = {1996}, editor = {{Rajeev Alur} and {Thomas A. Henzinger}}, volume = {1102}, series = {Lecture Notes in Computer Science}, pages = {428--432}, address = {New Brunswick, NJ, USA}, publisher = {Springer-Verlag}, abstract = {Manual abstraction can be performed by giving a file containing the names of variables to abstract. For each variable appearing in the file, a new primary input node is created to drive all the nodes that were previously driven by the variable. Abstracting a net effectively allows it to take any value in its range, at every clock cycle. Fair CTL model checking and language emptiness check VIS performs fair CTL model checking under Buchi fairness constraints. In addition, VIS can perform ...}, citeseerurl = {citeseer.ist.psu.edu/brayton96vis.html}, comment = {Proceedings of the Eighth International Conference on Computer Aided Verification}, keywords = {model checker}, url = {citeseer.ist.psu.edu/brayton96vis.html} } @ARTICLE{DBLP:journals/fmsd/CohenN09, author = {Ariel Cohen 0002 and Kedar S. Namjoshi}, title = {Local proofs for global safety properties}, journal = {Formal Methods in System Design}, year = {2009}, volume = {34}, pages = {104-125}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1007/s10703-008-0063-8}, keywords = {Refinement} } @ARTICLE{akers78, author = {B.~Akers}, title = {Binary Decision Diagrams}, journal = {IEEE Transactions on Computers}, year = {1978}, volume = {27}, pages = {509--516}, number = {6}, abstract = { The seminal paper in which BDD's were introduced. Note that none of the today implementation techniques for BDD package is given in this paper. }, keywords = {BDD description} } @INPROCEEDINGS{alfaro01interface, author = {L.~de Alfaro and T.A.~Henzinger}, title = {Interface automata}, booktitle = {ESEC/FSE-9: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering}, year = {2001}, pages = {109--120}, address = {New York, NY, USA}, publisher = {ACM Press}, doi = {http://doi.acm.org/10.1145/503209.503226}, isbn = {1-58113-390-1}, location = {Vienna, Austria} } @INPROCEEDINGS{bhdl03, author = {A.~Aljer and P.~Devienne and S.~Tison and J-L.~Boulanger and G.~Mariano}, title = {{BHDL: Circuit Design in B}}, booktitle = {ACSD '03: Proceedings of the Third International Conference on Application of Concurrency to System Design}, year = {2003}, editor = {IEEE Computer Society}, pages = {241}, address = {Washington, DC, USA}, isbn = {0-7695-1887-7} } @INPROCEEDINGS{alur99automating, author = {R. Alur and L.~de Alfaro and T. A. Henzinger and F.~Y.C. Mang}, title = {Automating Modular Verification}, booktitle = {CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings}, year = {1999}, editor = {Jos C. M. Baeten and Sjouke Mauw}, volume = {1664}, series = {Lecture Notes in Computer Science}, pages = {82-97}, address = {Eindhoven, The Netherlands}, publisher = {Springer}, abstract = {Modular techniques for automatic verification attempt to overcome the state-explosion problem by exploiting the modular structure naturally present in many system designs. Unlike other tasks in the verification of finite-state systems, current modular techniques rely heavily on user guidance. In particular, the user is typically required to construct module abstractions that are neither too detailed as to render insufficient benefits in state exploration, nor too coarse as to invalidate the desired system properties. In this paper, we construct abstract modules automatically, using reachability and controllability information about the concrete modules. This allows us to leverage automatic verification techniques by applying them in layers: first we compute on the state spaces of system components, then we use the results for constructing abstractions, and finally we compute on the abstract state space of the system. Our experimental results indicate that if reachability and controllabil ity information is used in the construction of abstractions, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification.}, file = {automatic_modular.pdf:/dsk/l1/misc/doc/modular/modular/automatic_modular.pdf:PDF}, keywords = {modular, abstraction, refinment loop, case study}, owner = {cecile}, timestamp = {2006.02.06}, url = {http://link.springer.de/link/service/series/0558/bibs/1664/16640082.htm} } @ARTICLE{DBLP:journals/fmsd/AlurH99b, author = {R.~Alur and T.A.~Henzinger}, title = {Reactive Modules.}, journal = {Formal Methods in System Design}, year = {1999}, volume = {15}, pages = {7-48}, number = {1}, bibsource = {DBLP, http://dblp.uni-trier.de}, publisher = {Springer} } @INPROCEEDINGS{alur98mocha, author = {R.~Alur and T.A.~Henzinger and F.Y. C.~Mang and S.~Qadeer and S.K.~Rajamani and S.~Tasiran}, title = {{MOCHA}: {M}odularity in {M}odel {C}hecking}, booktitle = {CAV'98: Proceedings of the 10th International Conference on Computer Aided Verification}, year = {1998}, volume = {1427}, series = {Lecture Notes in Computer Science}, pages = {521-525}, address = {London, UK}, abstract = {We describe a new interactive verification environment called Mocha for modular verification of heterogeneous systems. Mocha differs from existing model checkers in three important ways. First, instead of manipulating unstructured statetransition graphs, it supports the heterogeneous modeling framework of Reactive Modules. Second, instead of traditional temporal logics such as CTL, it uses Alternating Temporal Logic (ATL), a temporal logic that is designed to specify collaborative as ...}, file = {alur98mocha.ps.gz:/dsk/l1/misc/doc/modular/mocha/alur98mocha.ps.gz:PDF}, keywords = {model checker, atl, modular} } @INPROCEEDINGS{amla01assume, author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler}, title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams}, booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2001}, pages = {465--479}, address = {London, UK}, publisher = {Springer-Verlag}, isbn = {3-540-41865-2} } @ARTICLE{arieliA98value, author = {Ofer Arieli and Arnon Avron}, title = {The Value of the Four Values.}, journal = {Artif. Intell.}, year = {1998}, volume = {102}, pages = {97-141}, number = {1}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1016/S0004-3702(98)00032-0}, file = {arieli98four.ps:/dsk/l1/misc/doc/logique/arieli98four.ps:PDF}, keywords = {4-valued, logic} } @BOOK{arnold94finite, title = {Finite {T}ransition {S}ystems: {S}emantics of {C}ommunicating {S}ystems}, publisher = {Prentice Hall International Ltd.}, year = {1994}, editor = {Translator-John Plaice}, author = {A.~Arnold}, address = {Hertfordshire,UK}, isbn = {0-13-092990-5}, keywords = {simulation} } @ARTICLE{DBLP:journals/entcs/AwedhS06, author = {M.~Awedh and F.~Somenzi}, title = {Termination Criteria for Bounded Model Checking: Extensions and Comparison}, journal = {Electronic Notes in Theoritical Computer Science.}, year = {2006}, volume = {144}, pages = {51-66}, number = {1}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1016/j.entcs.2005.07.019}, file = {:BMC/TerminationCriteriaForBMC06.pdf:PDF}, keywords = {BMC, VIS} } @MANUAL{bmanual, title = {{B-Toolkit User's Manual}}, author = {{B-Core(UK) Ltd.}}, edition = {release 3.7}, year = {1997}, keywords = {b method}, owner = {cecile}, timestamp = {2006.07.31}, url = {http://www.b-core.com/downloading.html} } @INPROCEEDINGS{BP-msr03, author = {M.~Baclet and R.~Pacalet}, title = {V{\'e}rifications du protocole~{VCI}}, booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'03)}, year = {2003}, editor = {M{\'e}ry, Dominique and Rezg, Nidhal and Xie, Xiaolan}, pages = {431-445}, address = {Metz, France}, month = oct, publisher = {Herm{\`e}s}, keywords = {protocol}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/vci-msr03.ps} } @INPROCEEDINGS{broissyval, author = {F.~Badeau and A.~Amelot}, title = {{Using B as a High Level Programming Language in an Industrial Project: Roissy VAL}}, booktitle = {ZB 2005: Formal Specification and Development in Z and B}, year = {2005}, volume = {3455/2005}, series = {Lecture Notes in Computer Science}, pages = {334-354}, publisher = {Springer Berlin / Heidelberg}, doi = {10.1007/11415787_20}, keywords = {b method}, owner = {cecile}, timestamp = {2007.01.31}, url = {http://www.springerlink.com/content/x8mcgk2p8r82e2gl/} } @INPROCEEDINGS{503274, author = {T.~Ball and S.K.~Rajamani}, title = {The {SLAM} project: debugging system software via static analysis}, booktitle = {POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, year = {2002}, pages = {1--3}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/503272.503274}, isbn = {1-58113-450-9}, keywords = {CEGAR, refinment loop, model checking software}, location = {Portland, Oregon}, owner = {cecile}, timestamp = {2007.01.14} } @INPROCEEDINGS{rulebase96, author = {I.~Beer and S.~Ben-David and C.~Eisner and A.~Landver}, title = {{RuleBase: an industry-oriented formal verification tool}}, booktitle = {DAC '96: Proceedings of the 33rd annual conference on Design automation}, year = {1996}, series = {ACM Press}, pages = {655--660}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/240518.240642}, isbn = {0-89791-779-0}, location = {Las Vegas, Nevada, United States}, owner = {cecile}, timestamp = {2007.01.31} } @INPROCEEDINGS{1517440, author = {Bjesse, Per}, title = {Word-level sequential memory abstraction for model checking}, booktitle = {FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design}, year = {2008}, pages = {1--9}, address = {Piscataway, NJ, USA}, publisher = {IEEE Press}, file = {:Cegar/worllevelSeqMemAbstrforMCbjesse08.pdf:PDF}, isbn = {978-1-4244-2735-2}, keywords = {Abstractions, Model-checking}, location = {Portland, Oregon} } @TECHREPORT{prosyd05, author = {R. Bloem and B. Jobstmann and A. Pnueli.}, title = {{Property-based Logic Synthesis for Rapid Design Prototyping}}, institution = {Prosyd Deliverable D2.2/1}, year = {2005}, owner = {cecile}, timestamp = {2007.02.07} } @ARTICLE{bozga97protocol, author = {M.~Bozga and J-C.~Fernandez and A.~Kerbrat and L.~Mounier}, title = {Protocol {V}erification with the {ALD{\'E}BARAN} {T}oolset.}, journal = {STTT}, year = {1997}, volume = {1}, pages = {166-184}, number = {1-2}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://link.springer.de/link/service/journals/10009/bibs/7001001/70010166.htm}, keywords = {model checking, model checker}, publisher = {Springer} } @TECHREPORT{Brady:EECS-2008-136, author = {Brady, Bryan and Bryant, Randal and Seshia, Sanjit A.}, title = {Abstracting RTL Designs to the Term Level}, institution = {EECS Department, University of California, Berkeley}, year = {2008}, number = {UCB/EECS-2008-136}, month = {Oct}, abstract = {Term-level verification is a formal technique that seeks to verify RTL hardware descriptions by abstracting away details of data representations and operations. The key to making term-level verification automatic and efficient is in deciding what to abstract. We investigate this question in this paper and propose a solution based on the use of type qualifiers. First, we demonstrate through case studies that only selective term-level abstraction can be very effective in reducing the run-time of formal tools while still retaining precision of analysis. Second, the term-level abstraction process can be guided using lightweight type qualifiers. We present an annotation language and type inference scheme that is applied to the formal verification of the Verilog implementation of a chip multiprocessor router. Experimental results indicate type-based selective term-level abstraction is effective at scaling up verification with minimal designer guidance.}, file = {:Abstraction/abstractingRTLtoTermLevel.pdf:PDF}, keywords = {Abstraction, memory}, owner = {cecile}, timestamp = {2010.06.10}, url = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.html} } @PHDTHESIS{braunstein_phd07, author = {C.~Braunstein}, title = {"Conception Incrémentale, Vérification de Composants Matériels et Méthode d'abstraction pour la Vérification de Systèmes Intégrés sur Puce"}, school = {{Universitée Pierre et Marie Curie (Paris 6)}}, year = {2007}, address = {LIP6/SOC}, owner = {cecile}, timestamp = {2007.04.16} } @TECHREPORT{cecile03dea, author = {C.~Braunstein}, title = {{Transformation de propri\'et\'es CTL lors d'une m\'ethode de conception incr\'ementale des wrappers {VCI/PI}}}, institution = {LIP6/ASIM}, year = {2003}, type = {Rapport de {DEA}}, owner = {cecile}, timestamp = {2006.09.07} } @ARTICLE{braunstein06sttt, author = {C.~Braunstein and E.~Encrenaz}, title = {{CTL}-property {T}ransformations along an {I}ncremental {D}esign {P}rocess}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, year = {2007}, volume = {9}, pages = {77--88}, number = {1}, note = {A long version including the proof is available at www-asim.lip6.fr/~cecile}, owner = {cecile}, publisher = {Springer}, timestamp = {2006.09.05} } @INPROCEEDINGS{braunstein07acsd, author = {C.~Braunstein and E.~Encrenaz}, title = {Using CTL formulae as Component Abstraction in a Design and Verification Flow}, booktitle = {ACSD'07: Proceedings of the 7th International Conference on Application of Concurrency to System Design}, year = {2007}, note = {accepted}, keywords = {Abstraction, CEGAR, CTL}, owner = {cecile}, timestamp = {2007.03.27} } @INPROCEEDINGS{braunstein06lpar, author = {C.~Braunstein and E.~Encrenaz}, title = {A Further Step in the Incremental Design Process: Incorporation of an Increment Specification}, booktitle = {LPAR'06: Proceeding of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning}, year = {2006}, note = {{\it short paper}, proceedings online \url{http://www.lix.polytechnique.fr/~hermann/LPAR2006/}}, owner = {cecile}, timestamp = {2007.03.27} } @TECHREPORT{Braunstein_Encrenaz_RR_LIP6_07_2006, author = {C.~Braunstein and E.~Encrenaz}, title = {Using CTL formulae as component abstraction}, institution = {UPMC/LIP6}, year = {2006}, type = {Research report}, owner = {cecile}, timestamp = {2006.09.29} } @INPROCEEDINGS{pipeline06, author = {C.~Braunstein and E.~Encrenaz}, title = {Formalizing the Incremental Design and Verification Process of a Pipelined Protocol Converter}, booktitle = {RSP '06: Proceedings of the Seventeenth IEEE International Workshop on Rapid System Prototyping (RSP'06)}, year = {2006}, pages = {103--109}, address = {Washington, DC, USA}, publisher = {IEEE Computer Society}, doi = {http://dx.doi.org/10.1109/RSP.2006.19}, isbn = {0-7695-2580-6}, owner = {cecile}, timestamp = {2006.08.31} } @ARTICLE{avocs_incr, author = {C.~Braunstein and E.~Encrenaz}, title = {{CTL}-{P}roperty {T}ransformations along an {I}ncremental {D}esign {P}rocess}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2005}, volume = {128}, pages = {263--278}, number = {6}, file = {braunstein_avocs_o4.pdf:/dsk/l1/misc/Article/Concep_incr/Avocs/Avocs_paper/braunstein_avocs_o4.pdf:PDF}, issue = {6}, publisher = {Elsevier}, series = {AVOCS'04~-~Proceedings of the 4th International Workshop on Automated Verification of Critical Systems} } @ARTICLE{browneclarkegrum88, author = {M.C.~Browne and E.M.~Clarke and O.~Grumberg}, title = {Characterizing {F}inite {K}ripke {S}tructures in {P}ropositional {T}emporal {L}ogic}, journal = {Theoritical Computer Science}, year = {1988}, volume = {59}, pages = {115--131}, number = {1-2}, doi = {http://dx.doi.org/10.1016/0304-3975(88)90098-9}, issn = {0304-3975}, publisher = {Elsevier Science Publishers Ltd.} } @ARTICLE{Bryant86, author = {R.E.~Bryant}, title = {{Graph-Based Algorithms for Boolean Function Manipulation}}, journal = {IEEE Transactions on Computers}, year = {1986}, volume = {35}, pages = {677-691}, number = {8}, bibsource = {DBLP, http://dblp.uni-trier.de}, keywords = {BDD}, owner = {cecile}, timestamp = {2006.11.07} } @INPROCEEDINGS{bunker:idpt02, author = {A.~Bunker and G.~Gopalakrishnan}, title = {{Verifying a VCI Bus Interface Model Using an LSC-based Specification}}, booktitle = {Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology}, year = {2002}, editor = {H. Ehrig and B. J. Kr\"amer and A. Ertas}, pages = {48}, month = {June}, organization = {Society of Design and Process Science}, keywords = {protocol}, url = {http://www.engineering.usu.edu/ece/faculty/bunker/pubs/idpt02.pdf} } @ARTICLE{macmillan, author = {J.R.~Burch and E.M.~Clarke and K.L.~McMillan and D.L.~Dill and L.J.~Hwang}, title = {Symbolic {M}odel {C}hecking: $10^{20}$ {S}tates and {B}eyond}, journal = {{I}nformation and {C}omputation }, year = {1992}, volume = {98}, pages = {142--170}, number = {2}, note = {Special issue for best papers from LICS'90}, address = {Duluth, MN, USA}, publisher = {Academic Press, Inc.} } @INPROCEEDINGS{burch94automatic, author = {J.R.~Burch and D.L.~Dill}, title = {Automatic {V}erification of {P}ipelined {M}icroprocessors {C}ontrol}, booktitle = {Proceedings of the sixth International Conference on Computer-Aided Verification {CAV'94}}, year = {1994}, editor = {{D.L.~Dill}}, volume = {LNCS 818}, pages = {68--80}, address = {Standford, California, USA}, publisher = {Springer-Verlag}, citeseerurl = {citeseer.ist.psu.edu/burch94automatic.html}, keywords = {model checking, pipeline, archi}, url = {citeseer.ist.psu.edu/burch94automatic.html} } @ARTICLE{bryant82, author = {J.R.~Burch and D.L.~Dill}, title = {Graph-Based Algorithms for Boolean Function Manipulation}, journal = {IEEE Transactions on Computers}, year = {1982}, volume = {35}, pages = {677--691}, number = {8}, month = {August}, abstract = {Available} } @INPROCEEDINGS{Cabodi09Speeding, author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco and S. Quer}, title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints}, booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe}, year = {2009}, pages = {1686-1691}, file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF}, keywords = {Composition , model checking}, owner = {cecile}, timestamp = {2009.04.30} } @INCOLLECTION{Cansell2001AbstractionandRefinementofFeatures, author = {D.~Cansell and D.~M{\'e}ry}, title = {Abstraction and {R}efinement of {F}eatures}, booktitle = {{Language Constructs for Designing Features}}, publisher = {Springer-Verlag}, year = {2001}, editor = {S.~Gilmore and M.~Ryan}, pages = {65--84}, abstract = {The composition of services and features often leads to unwanted situations, because it is a non-monotonic operation over services and features. When a new service is added to an existing system, conditions have to be checked to ensure that the resulting system satisfies a list of required properties. Following the system approach of Abrial, we develop services and features in an incremental way and use refinement to model the composition of services and features. Proof obligations state the preservation or the non-preservation of properties, namely invariant or more generally safety properties. The method helps us in understanding when a service is interfering with another, and allows us to give multiple views of each service according to the level of its refinement. Finally, we validate our method with the Atelier B tool.} } @INCOLLECTION{cassez-proving, author = {F.~Cassez and M.~Ryan and P-Y.~Schobbens}, title = {Proving {F}eature {N}on-{I}nteraction with {A}lternating-{T}ime {T}emporal {L}ogic}, booktitle = {{Language Constructs for Describing Features}}, publisher = {Springer Verlag}, year = {2001}, editor = {S.~Gilmore and M.~Ryan}, pages = {85--104} } @ARTICLE{chechik03multi, author = {M.~Chechik and B.~Devereux and S.~M.~Easterbrook and A.~Gurfinkel}, title = {{Multi-Valued Symbolic Model-Checking}}, journal = {ACM Transactions on Software Engineering and Methodology}, year = {2003}, volume = {12}, pages = {371-408}, number = {4}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.acm.org/10.1145/990010.990011}, file = {chechik03a.pdf:/dsk/l1/misc/doc/abstraction/chechik03a.pdf:PDF}, keywords = {abstraction, 3-valued, 4-valued, logic, model checking} } @INPROCEEDINGS{846816, author = {Hoon Choi and Myung-Kyoon Yim and Jae-Young Lee and Byeong-Whee Yun and Yun-Tae Lee}, title = {Formal Verification of an Industrial System-on-a-Chip}, booktitle = {ICCD '00: Proceedings of the 2000 IEEE International Conference on Computer Design}, year = {2000}, pages = {453}, address = {Washington, DC, USA}, publisher = {IEEE Computer Society}, isbn = {0-7695-0801-4}, keywords = {AMBA} } @INPROCEEDINGS{CLS00, author = {G. Ciardo and G. L\"uttgen and R. Siminiceanu}, title = {Efficient Symbolic State-Space Construction for Asynchronous Systems}, booktitle = {Proc. of ICATPN'2000}, year = {2000}, volume = {1825}, series = {Lecture Notes in Computer Science}, pages = {103--122}, publisher = {Springer Verlag} } @ARTICLE{cimatti00nusmv, author = {A.~Cimatti and E.M.~Clarke and F.~Giunchiglia and M.~Roveri}, title = {NUSMV: A New Symbolic Model Checker.}, journal = {STTT}, year = {2000}, volume = {2}, pages = {410-425}, number = {4}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://link.springer.de/link/service/journals/10009/bibs/0002004/00020410.htm} } @ARTICLE{DBLP:journals/tocl/CimattiGS10, author = {Alessandro Cimatti and Alberto Griggio and Roberto Sebastiani}, title = {Efficient generation of craig interpolants in satisfiability modulo theories}, journal = {ACM Trans. Comput. Log.}, year = {2010}, volume = {12}, pages = {7}, number = {1}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.acm.org/10.1145/1838552.1838559} } @ARTICLE{Clarke1986, author = {E.M.~Clarke and E.A.~Emerson and A.P.~Sistla}, title = {Automatic verification of finite-state concurrent systems using temporal logic specifications}, journal = {ACM Transactions on Programming Languages and Systems}, year = {1986}, volume = {8}, pages = {244--263}, number = {2}, booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets}, doi = {http://doi.acm.org/10.1145/5397.5399}, issn = {0164-0925}, publisher = {ACM Press} } @ARTICLE{clarke94model, author = {E.M.~Clarke and O.~Grumberg and D.E.~Long}, title = {{Model Checking and Abstraction}}, journal = {ACM Transactions on Programming Languages and Systems}, year = {1994}, volume = {16}, pages = {1512--1542}, number = {5}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/186025.186051}, issn = {0164-0925}, keywords = {model cheking, abstraction, CTL, preservation}, publisher = {ACM Press} } @BOOK{clarke99model, title = {Model Checking}, publisher = {The {MIT} {P}ress}, year = {1999}, author = {E.M.~Clarke and O.~Grumberg and D.A.~Peled}, address = {Cambridge, Massachusetts}, isbn = {0-262-03270-8}, keywords = {CTL,LTL, model checking,kripke structure, simulation} } @ARTICLE{Clarke03cegarsymbolic, author = {E.~M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith}, title = {Counterexample-guided bstraction refinement for symbolic model checking.}, journal = {Journal of the ACM}, year = {2003}, volume = {50}, pages = {752-794}, number = {5}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.acm.org/10.1145/876638.876643}, file = {:Cegar/Counterexample-guided abstraction refinement.pdf:PDF}, keywords = {abstraction, CEGAR}, owner = {cecile}, timestamp = {2006.06.27} } @INPROCEEDINGS{DBLP:conf/dac/ClarkeGMZ95, author = {Edmund M. Clarke and Orna Grumberg and Kenneth L. McMillan and Xudong Zhao}, title = {Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking}, booktitle = {DAC}, year = {1995}, pages = {427-432}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.acm.org/10.1145/217474.217565} } @ARTICLE{DBLP:journals/tcad/ClarkeGS04, author = {Edmund M. Clarke and Anubhav Gupta and Ofer Strichman}, title = {SAT-based counterexample-guided abstraction refinement}, journal = {IEEE Trans. on CAD of Integrated Circuits and Systems}, year = {2004}, volume = {23}, pages = {1113-1123}, number = {7}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.ieeecomputersociety.org/10.1109/TCAD.2004.829807}, file = {:Cegar/SATBasedCegar2004Clarke.pdf:PDF}, keywords = {CEGAR,SAT}, owner = {cecile}, timestamp = {2010.06.03} } @MISC{tata97, author = {H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D. Lugiez and S. Tison and M. Tommasi}, title = {Tree Automata Techniques and Applications}, howpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}}, year = {1997}, note = {release October, 1rst 2002}, file = {tata.pdf:/dsk/l1/misc/doc/automate/tata.pdf:PDF}, keywords = {tree automata} } @INPROCEEDINGS{madre, author = {O.~Coudert and J.-C.~Madre}, title = {A New Method to Compute Prime and Essential Prime Implicants of Boolean Functions}, booktitle = {Advanced Research in VLSI and Parallel Systems}, year = {1992}, editor = {T.~Knight and J.~Savage}, pages = {113--128}, month = {March}, abstract = { This paper presents how prime implicants and essential prime implicants can be computed by means of meta-products encoded with of BDD's. It gives the equations that mimic the definitions, but it does not propose a recursive algorithm. The variable ordering is discussed and experimental results are provided that come from a benchmark of circuits. }, keywords = {Prime Implicants} } @INPROCEEDINGS{DBLP:conf/popl/CousotC77, author = {P.~Cousot and R.~Cousot}, title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.}, booktitle = {POPL'77: Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages}, year = {1977}, pages = {238-252}, address = {Munich, Germany}, bibsource = {DBLP, http://dblp.uni-trier.de}, keywords = {abstraction}, owner = {cecile}, timestamp = {2007.01.13} } @INPROCEEDINGS{jmc-ag-djs:ddd, author = {J.M.~Couvreur and A.~Griffault and D.J.~Sherman}, title = {Diagrammes de d\'ecision pour la v\'erification de r\'eseaux \`a files}, booktitle = {Mod\'elisation de syst\`emes r\'eactifs (MSR'99)}, year = {1999}, address = {ENS Cachan}, month = {March} } @INPROCEEDINGS{CA94, author = {J.M. Couvreur and E. Paviot-Adet}, title = {New Structural Invariants for {P}etri Nets Analysis}, booktitle = {Proc. of ICATPN'94}, year = {1994}, volume = {815}, series = {Lecture Notes in Computer Science}, pages = {199--218}, publisher = {Springer Verlag} } @ARTICLE{dams97abstract, author = {D.~Dams and R.~Gerth and O.~Grumberg}, title = {Abstract interpretation of reactive systems}, journal = {ACM Transactions on Programming Languages and Systems}, year = {1997}, volume = {19}, pages = {253--291}, number = {2}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/244795.244800}, issn = {0164-0925}, keywords = {abstraction}, publisher = {ACM Press} } @INPROCEEDINGS{Darbari08transient, author = {Darbari, A. and Al Hashimi, B. and Harrod, P. and Bradley, D.}, title = {A New Approach for Transient Fault Injection Using Symbolic Simulation}, booktitle = {IEEE International Symposium On-line Testing Symposium}, year = {2008}, pages = {93-98}, month = {July}, doi = {10.1109/IOLTS.2008.59}, journal = {On-Line Testing Symposium, 2008. IOLTS '08. 14th IEEE International}, keywords = {fault tolerance, fault trees, reduced instruction set computing, temporal logicbinary image, multicycle RISC processor, program image. shadow, symbolic simulation, transient fault injection} } @MISC{duret03dea, author = {A.~Duret-Lutz and R.~Rebiha}, title = {SPOT : Une bibliothèque de vérificaion de propriétés de logique temporelle à temps linéaire}, year = {2003}, file = {rap_stage_duret_lutz_2003.pdf:/dsk/l1/misc/doc/ltl_auto/rap_stage_duret_lutz_2003.pdf:PDF}, keywords = {LTL, automata approach}, owner = {cecile}, timestamp = {2006.02.13} } @INPROCEEDINGS{dwyer99patterns, author = {M. B. Dwyer and G. S. Avrunin and J. C. Corbett}, title = {{Patterns in Property Specifications for Finite-State Verification.}}, booktitle = {ICSE' 99. Proceedings of the 1999 International Conference on Software Engineering}, year = {1999}, editor = {ACM}, pages = {411-420}, address = {Los Angeles, CA, USA}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://portal.acm.org/citation.cfm?id=302405.302672}, keywords = {CTL , patterns , Specification}, url = {http://patterns.projects.cis.ksu.edu/collaborations/papers.shtml} } @INPROCEEDINGS{6128043, author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho}, title = {Automatic Service Composition via Model Checking}, booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific}, year = {2011}, pages = {477 -482}, month = {dec.}, abstract = {Web service composition is the process of constructing a set of Web services which, when invoked with some user input in a particular order, can produce the output to the user's requirements. This paper proposes a novel model checking based approach for automated service composition. Modeling services as a set of interleaved processes in a class of process algebra, we formulate service composition as model checking asserted on a specific type of property on the model. We show that, under this formulation, correct composition workflows can be constructed from the counter-examples provided by model checking. With a case study on online hotel booking services, we demonstrate that the proposed approach can support directed a cyclic composition graphs and the generated composition graphs are automatically verified.}, doi = {10.1109/APSCC.2011.54}, file = {:/users/outil/verif/biblio/Composition/AutomaticServiceCompositionViaModelChecking2011.pdf:PDF}, keywords = {Web service composition;automated service composition;directed acyclic composition graph;interleaved process;model checking;online hotel booking services;process algebra;user requirements;Web services;directed graphs;formal verification;hotel industry;process algebra;}, owner = {cecile}, timestamp = {2012.03.07} } @ARTICLE{DBLP:journals/tcad/FeySBD08, author = {G{\"o}rschwin Fey and Stefan Staber and Roderick Bloem and Rolf Drechsler}, title = {Automatic Fault Localization for Property Checking}, journal = {IEEE Trans. on CAD of Integrated Circuits and Systems}, year = {2008}, volume = {27}, pages = {1138-1149}, number = {6}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1109/TCAD.2008.923234} } @ARTICLE{fitting91bilattices, author = {M.~Fitting}, title = {{Bilattices and the Semantics of Logic Programming.}}, journal = {Journal of Logic Programming}, year = {1991}, volume = {11}, pages = {91-116}, number = {1{\&}2}, bibsource = {DBLP, http://dblp.uni-trier.de}, file = {BilSemLP.pdf:/dsk/l1/misc/doc/logique/BilSemLP.pdf:PDF}, keywords = {4-valued, logic, 3-valued}, owner = {cecile}, timestamp = {2006.04.05} } @INPROCEEDINGS{godefroid03expressiveness, author = {Patrice Godefroid and Radha Jagadeesan}, title = {On the Expressiveness of 3-Valued Models}, booktitle = {VMCAI 2003: Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation}, year = {2003}, pages = {206--222}, address = {London, UK}, publisher = {Springer-Verlag}, file = {vmcai2003.ps:/dsk/l1/misc/doc/logique/vmcai2003.ps:PDF}, isbn = {3-540-00348-7}, keywords = {3-valued, logic, model checking, Kripke structure} } @INPROCEEDINGS{goelL00formal, author = {A.~Goel and W.~R.~Lee}, title = {{{F}ormal {V}erification of an {IBM} {C}ore{C}onnect {P}rocessor {L}ocal {B}us {A}rbiter {C}ore}}, booktitle = {DAC'00: Proceedings of the 37th Conference on Design Automation}, year = {2000}, editor = {ACM}, pages = {196-200}, address = {Los Angeles, CA, USA}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.acm.org/10.1145/337292.337384}, file = {p196-goel.pdf:/dsk/l1/misc/doc/verif_archi/rulebase/p196-goel.pdf:PDF}, keywords = {CTL, model checking, Rulebase}, owner = {cecile}, timestamp = {2006.06.29} } @INPROCEEDINGS{GL91, author = {O.~Grumberg and D.E.~Long}, title = {Model {C}hecking and {M}odular {V}erification}, booktitle = {International Conference on Concurrency Theory}, year = {1991}, volume = {527}, series = {Lecture Notes in Computer Science}, pages = {250--263}, publisher = {Springer Verlag}, file = {p843-grumberg.pdf:/dsk/l1/misc/doc/modular/model_checking/p843-grumberg.pdf:PDF}, keywords = {simulation,CTL, modular} } @ARTICLE{Gupta92syrvey, author = {A.~Gupta}, title = {{Formal Hardware Verification Methods: A Survey.}}, journal = {Formal Methods in System Design}, year = {1992}, volume = {1}, pages = {151-238}, number = {2/3}, bibsource = {DBLP, http://dblp.uni-trier.de}, keywords = {survey, hardware, formal verification} } @INPROCEEDINGS{henzinger99dsp, author = {T.~A.~Henzinger and X.~Liu and S.~Qadeer and S.~K.~Rajamani}, title = {Formal {S}pecification and {V}erification of a {D}ataflow {P}rocessor {A}rray.}, booktitle = {I{CCAD}'99: {P}roceedings of the 1999 {IEEE}/{ACM} {I}nternational {C}onference on {C}omputer-{A}ided {D}esign}, year = {1999}, editor = {Jacob K. White, Ellen Sentovich}, pages = {494-499}, address = {San Jose, USA}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://portal.acm.org/citation.cfm?id=339492.340066}, file = {formal_specification_and_verification_of_a_dataflow_processor_array.pdf:/dsk/l1/misc/doc/modular/mocha/formal_specification_and_verification_of_a_dataflow_processor_array.pdf:PDF}, keywords = {abstraction, assume-guarantee, ATL, modular, archi, MOCHA} } @INPROCEEDINGS{henzinger00decomposing, author = {Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani}, title = {Decomposing refinement proofs using assume-guarantee reasoning}, booktitle = {ICCAD '00: Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design}, year = {2000}, pages = {245--253}, address = {San Jose, California}, publisher = {IEEE Press}, file = {decomposing00henzinger.pdf:/dsk/l1/misc/doc/modular/assume/decomposing00henzinger.pdf:PDF}, isbn = {0-7803-6448-1} } @INPROCEEDINGS{C:HJMS03, author = {Henzinger, T.A. and Jhala, R. and Majumdar, R. and Sutre, G.}, title = {Software {V}erification with {BLAST}}, booktitle = {SPIN'2003: Proceedings of the 10th International SPIN Workshop}, year = {2003}, volume = {2648}, series = {Lecture Notes in Computer Science}, pages = {235--239}, address = {USA}, publisher = {Springer}, note = {Tool paper}, keywords = {software, model-checking}, url = {http://www.labri.fr/publications/mvtsi/2003/HJMS03} } @INPROCEEDINGS{henzinger98you, author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani}, title = {{Y}ou {A}ssume, {W}e {G}uarantee: {M}ethodology and {C}ase {S}tudies}, booktitle = {C{AV}'98: {P}roceedings of the 10th {I}nternational {C}onference on {C}omputer {A}ided {V}erification}, year = {1998}, editor = {Alan J. Hu, Moshe Y. Vardi}, volume = {1427}, series = {Lecture Notes in Computer Science}, pages = {440--451}, address = {Vancouver, Canada}, publisher = {Springer-Verlag}, file = {henzinger98you.ps.gz:/dsk/l1/misc/doc/modular/assume/henzinger98you.ps.gz:PDF} } @ARTICLE{henzinger02anassume, author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani and S.~Tasiran}, title = {An {A}ssume-{G}uarantee {R}ule for {C}hecking {S}imulation}, journal = {ACM Transactions on Programming Languages Systems}, year = {2002}, volume = {24}, pages = {51--64}, number = {1}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/509705.509707}, file = {henzinger98assumeguarantee.ps:/dsk/l1/misc/doc/modular/assume/henzinger98assumeguarantee.ps:PDF}, issn = {0164-0925}, publisher = {ACM Press} } @ARTICLE{Holzmann97e, author = {G.J.~Holzmann}, title = {{The Model Checker Spin}}, journal = {IEEE Transactions on Software Engineering}, year = {1997}, volume = {23}, pages = {279--295}, number = {5}, month = {May}, note = {Special issue on Formal Methods in Software Practice} } @INPROCEEDINGS{hosabettu98decomposing, author = {R.~Hosabettu and M.~Srivas and G.~Gopalakrishnan}, title = {Decomposing the {P}roof of {C}orrectness of {P}ipelined {M}icroprocessors}, booktitle = {Computer-Aided Verification, {CAV'98}}, year = {1998}, editor = {Alan J. Hu and Moshe Y. Vardi}, volume = {1427}, pages = {122--134}, address = {Vancouver, Canada}, publisher = {Springer-Verlag}, url = {citeseer.ist.psu.edu/208243.html} } @ARTICLE{huggins98spec, author = {J.K.~Huggins and D.~Van Campenhout}, title = {Specification and {V}erification of {P}ipelining in the {ARM2 RISC} {M}icroprocessor}, journal = {ACM Transactions on Design Automation of Electronic Systems}, year = {1998}, volume = {3}, pages = {563--580}, number = {4}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/296333.296345}, issn = {1084-4309}, publisher = {ACM Press} } @ARTICLE{HWA99, author = {H.~Hulgaard and P.~F.~Williams and H.~R.~Andersen}, title = {Equivalence Checking of Combinational Circuits using Boolean Expression Diagrams}, journal = {{IEEE} Transactions of Computer-Aided Design}, year = {1999}, volume = {18}, pages = {903-917}, number = {7}, month = {July} } @ARTICLE{DBLP:journals/tcad/JainKSC08, author = {H.~Jain and D.~Kroening and N.~Sharygina and E.M.~Clarke}, title = {Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog}, journal = {IEEE Transaction on CAD of Integrated Circuits and Systems}, year = {2008}, volume = {27}, pages = {366-379}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1109/TCAD.2007.907270}, file = {:Cegar/WLPredicateAbstractionRefinment08.pdf:PDF}, keywords = {Cegar, predicate abstraction, SAT} } @INPROCEEDINGS{kroening07vcegar, author = {H.~Jain and D.~Kroening and N.~Sharygina and E.~Clarke}, title = {{{VCEGAR}: Verilog CounterExample Guided Abstraction Refinement}}, booktitle = {T{ACAS}'07: {P}roceedings of the 13th {I}nternational {C}onference on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of {S}ystems}, year = {2007}, note = {Accepted paper}, owner = {cecile}, timestamp = {2007.02.07} } @INPROCEEDINGS{JainNFS97survey, author = {J.~Jain and A.~Narayan and M.~Fujita and A.L.~Sangiovanni-Vincentelli}, title = {A Survey of Techniques for Formal Verification of Combinational Circuits.}, booktitle = {ICCD}, year = {1997}, pages = {445-454}, bibsource = {DBLP, http://dblp.uni-trier.de}, keywords = {survey, hadware, formal veriication} } @ARTICLE{kalushy93knowledge, author = {Yuri Kaluzhny and Alexei Yu. Muravitsky}, title = {A knowledge representation based on the Belnap's four-valued logic}, journal = {Journal of Applied Non-Classical Logics}, year = {1993}, volume = {3}, pages = {189-203}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de}, file = {kaluzhny93knowledge.pdf:/dsk/l1/misc/doc/logique/kaluzhny93knowledge.pdf:PDF}, keywords = {CTL , abstraction , 3-valued , refinment loop}, owner = {cecile}, timestamp = {2006.04.03} } @INPROCEEDINGS{park03satunbounded, author = {H.-J.~Kang and I.-C.~Park}, title = {SAT-based Unbounded Symbolic Model Checking}, booktitle = {DAC'03: Proceedings of the 40th conference on Design automation}, year = {2003}, pages = {840--843}, address = {New York,USA}, publisher = {ACM}, doi = {http://doi.acm.org/10.1145/775832.776043}, file = {:BMC/kang03satunbounded.pdf:PDF;:BMC/Park05satUnbound.pdf:PDF}, isbn = {1-58113-688-9}, keywords = {SAT, all-sat}, location = {Anaheim, CA, USA} } @ARTICLE{Kern99survey, author = {C.~Kern and M.R.~Greenstreet}, title = {Formal {V}erification in {H}ardware {D}esign: a {S}urvey}, journal = {ACM Transactions on Design Automation of Electronic Systems}, year = {1999}, volume = {4}, pages = {123--193}, number = {2}, address = {New York, NY, USA}, doi = {http://doi.acm.org/10.1145/307988.307989}, issn = {1084-4309}, keywords = {survey, hadware, formal veriication}, publisher = {ACM Press} } @BOOK{kleene52introduction, title = {Introduction to Metamathematics}, publisher = {North-Holland}, year = {1952}, author = {Kleene, S.}, series = {Bibliotheca mathematica}, owner = {cecile}, timestamp = {2006.04.27} } @INPROCEEDINGS{KLM93, author = {T. Kolks and B. Lin and H. De Man}, title = {Sizing and Verification of Communication Buffers for Communicating Processes}, booktitle = {Proc. of IEEE International Conference on Computer-Aided Design}, year = {1993}, volume = {1825}, pages = {660--664}, address = {Santa Clara, USA} } @INPROCEEDINGS{kroening01automated, author = {D.~Kroening and W.J.~Paul}, title = {Automated {P}ipeline {D}esign}, booktitle = {DAC '01: Proceedings of the 38th conference on Design Automation}, year = {2001}, pages = {810--815}, publisher = {ACM Press}, doi = {http://doi.acm.org/10.1145/378239.379071}, isbn = {1-58113-297-2}, location = {Las Vegas, Nevada, United States} } @BOOK{kropf99introduction, title = {Introduction to Formal Hardware Verification}, publisher = {Springer Verlag}, year = {1999}, author = {T.~Kropf}, address = {Secaucus, NJ, USA}, isbn = {3540654453}, keywords = {survey, hardware}, owner = {cecile}, timestamp = {2006.11.07} } @ARTICLE{KupfermanG96branching, author = {O.~Kupferman and O.~Grumberg}, title = {Branching-Time Temporal Logic and Tree Automata.}, journal = {Information and Computation}, year = {1996}, volume = {125}, pages = {62-69}, number = {1}, bibsource = {DBLP, http://dblp.uni-trier.de}, file = {branchingand automata.ps:/dsk/l1/misc/doc/ctl_auto/branchingand automata.ps:PDF}, keywords = {CTL, tree automata ,model checking, automata approach} } @ARTICLE{KupfermanVW00automata, author = {O.~Kupferman and M.Y.~Vardi and P.~Wolper}, title = {An {A}utomata-{T}heoretic {A}pproach to {B}ranching-{T}ime {M}odel {C}hecking.}, journal = {Journal of the ACM}, year = {2000}, volume = {47}, pages = {312-360}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://doi.acm.org/10.1145/333979.333987}, file = {an-automata-theoretic-approach.pdf:/dsk/l1/misc/doc/automate/an-automata-theoretic-approach.pdf:PDF}, keywords = {tree automata, CTL, automata approach}, owner = {cecile}, timestamp = {2006.06.27} } @INPROCEEDINGS{lamp83, author = {L.~Lamport}, title = {Information Processing}, booktitle = {What good is in temporal logic}, year = {1983}, pages = {657--668}, publisher = {Elsevier} } @BOOK{Lano, title = {The {B} {L}anguage and {M}ethod, {A} {G}uide to {P}ractical {F}ormal {D}evelopment}, publisher = {Springer-Verlag}, year = {1996}, author = {K.~Lano}, series = {FACIT}, address = {UK}, keywords = {b method} } @INPROCEEDINGS{693769, author = {K.G~Larsen and B.~Steffen and C.~Weise}, title = {A Constraint Oriented Proof Methodology Based on Modal Transition Systems}, booktitle = {TACAS '95: Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems}, year = {1995}, pages = {17--40}, address = {London, UK}, publisher = {Springer-Verlag}, isbn = {3-540-60630-0} } @ARTICLE{LiWS05PureSat, author = {B.~Li and C.~Wang and F.~Somenzi}, title = {Abstraction Refinement in Symbolic Model Checking using Satisfiability as the Only Decision Procedure}, journal = {STTT}, year = {2005}, volume = {7}, pages = {143-155}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1007/s10009-004-0169-2}, file = {:Cegar/Li04PureSatSTTT.pdf:PDF}, keywords = {CEGAR, SAT} } @INCOLLECTION{springerlink:10.1007/978-3-540-68073-4_4, author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu}, title = {Component-Based Abstraction and Refinement}, booktitle = {High Confidence Software Reuse in Large Systems}, publisher = {Springer Berlin / Heidelberg}, year = {2008}, editor = {Mei, Hong}, volume = {5030}, series = {Lecture Notes in Computer Science}, pages = {39-51}, note = {10.1007/978-3}, affiliation = {Portland State University Dept. of Computer Science Portland OR 97207}, file = {:/users/outil/verif/biblio/Composition/Compponent-Based AbstractionRefinement2008.pdf:PDF}, isbn = {978-3-540-68062-8}, keyword = {Computer Science}, keywords = {Composition, Abstraction, Refinement, verified component, Hardware/software coverification}, url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4} } @INPROCEEDINGS{lin91implicit, author = {B.~Lin and A.R.~Newton}, title = {Implicit Manipulation of Equivalence Classes Using Binary Decision Diagrams}, booktitle = {ICCD '91: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer \& Processors}, year = {1991}, pages = {81--85}, address = {Washington, DC, USA}, publisher = {IEEE Computer Society}, isbn = {0-8186-2270-9} } @ARTICLE{Loiseaux, author = {C.~Loiseaux and S.~Graf and J.~Sifakis and A.~Bouajjani and S.~Bensalem}, title = {Property {P}reserving {A}bstractions for the {V}erification of {C}oncurrent {S}ystems}, journal = {Formal Methods in System Design}, year = {1995}, volume = {6}, pages = {11--44}, number = {1}, address = {Hingham, MA, USA}, publisher = {Kluwer Academic Publisher} } @INCOLLECTION{springerlink:10.1007/978-3-642-16901-4_15, author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng}, title = {Assume-Guarantee Reasoning with Local Specifications}, booktitle = {Formal Methods and Software Engineering}, publisher = {Springer Berlin / Heidelberg}, year = {2010}, editor = {Dong, Jin and Zhu, Huibiao}, volume = {6447}, series = {Lecture Notes in Computer Science}, pages = {204-219}, note = {10.1007/978-3-642-16901-4_15}, abstract = {We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee rule that permits reasoning about individual modules for local specifications and draws conclusions on global specifications. We illustrate our approach with an example from the field of network congestion control, where different agents are responsible for controlling packet flow across a shared infrastructure. In this context, we derive an assume-guarantee rule for system stability, and show that this rule is valuable to reason about any number of agents, any initial flow configuration, and any topology of bounded degree.}, affiliation = {Department of Computing, Imperial College London, UK}, file = {:/users/outil/verif/biblio/Composition/AGRwithLocalSpecification2010.pdf:PDF}, isbn = {978-3-642-16900-7}, keyword = {Computer Science}, keywords = {Compositional reasoning, composition}, owner = {cecile}, timestamp = {2012.03.07}, url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15} } @PHDTHESIS{long93thesis, author = {D.~E.~Long}, title = {Model {C}hecking, {A}bstraction, and {C}ompositional {V}erification}, school = {Carnegie Mellon University}, year = {1993}, file = {long93model.ps.gz:/dsk/l1/misc/doc/modular/model_checking/long93model.ps.gz:PDF}, keywords = {abstraction, CTL, modular, simulation, model checking}, owner = {cecile}, timestamp = {2006.03.08} } @INPROCEEDINGS{santo, author = {S.~Malik and A.R.~Wang and R.K~Brayton and A.~Sangiovanni-Vincentelli}, title = {Logic Verification using Binary Decision Diagrams in Logic Synthesis Environment}, booktitle = {Proceedings of the IEEE International Conference on Computer Aided Design, ICCAD'88}, year = {1988}, pages = {6--9}, month = {November}, note = {Santa Clara CA, USA}, abstract = { This paper proposes two heuristics for variable ordering based on the topology of the circuit under study. \begin{enumerate} \item One defines the level of a variable or a gate as follows: $level(root)=0$ and $level(f)=max(level(g))+1$, where the $g$'s are the fathers of $f$. The first heuristics consists in indexing the variables according to the decreasing order of their levels. The justification is that the influence of variables high in the circuit must be computed as soon as possible. \item Same as the previous heuristics but respecting modules. Modules are treated in the decreasing order of their depths. The depth of a formula being the maximum depth of its variables. \end{enumerate} Experimental results are reported, showing that the second heuristics is very good (on the ICSAS'85 benchmark). Lu }, keywords = {Variable ordering heuristics, Combinatorial Circuits} } @INPROCEEDINGS{manolios00correctness, author = {P.~Manolios}, title = {Correctness of Pipelined Machines}, booktitle = {FMCAD '00: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design}, year = {2000}, pages = {161--178}, publisher = {Springer-Verlag}, url = {citeseer.ist.psu.edu/426677.html} } @INPROCEEDINGS{manolios04web, author = {P.~Manolios and S.K.~Srinivasan}, title = {Automatic {V}erification of {S}afety and {L}iveness for {XS}cale-{L}ike {P}rocessor {M}odels {U}sing {WEB} Refinements}, booktitle = {DATE '04: Proceedings of the conference on Design, Automation and Test in Europe}, year = {2004}, pages = {168-174}, address = {Washington, DC, USA}, publisher = {IEEE Computer Society}, isbn = {0-7695-2085-5-1} } @INPROCEEDINGS{Mariano2002formalization, author = {G.~Mariano and J-L.~Boulanger and A. Aljer}, title = {Formalization of {D}igital {C}ircuits {U}sing the {B} {M}ethod}, booktitle = {Comp{R}ail {VIII}: 8th {I}nternational {C}onference on {C}omputer {A}ided {D}esign, {M}anufacture and {O}peration in the {R}ailway and other {A}dvanced {M}ass {T}ransit {S}ystems}, year = {2002}, address = {Lemnos, Greece}, month = {12 - 14 } # jun, keywords = {B method, formal development, software verification, safety-critical applications, VHDL, BHDL, Hardware}, url = {http://www.wessex.ac.uk/conferences/2002/cr02/} } @INPROCEEDINGS{Silva00Sat, author = {Marques-Silva, Jo\, {a}o P. and Sakallah, Karem A.}, title = {Boolean satisfiability in electronic design automation}, booktitle = {DAC '00: Proceedings of the 37th Annual Design Automation Conference}, year = {2000}, pages = {675--680}, address = {New York, NY, USA}, publisher = {ACM}, doi = {http://doi.acm.org/10.1145/337292.337611}, file = {:SAT/p675-marques-silva.pdf:PDF}, isbn = {1-58113-187-9}, keywords = {SAT, circuit}, location = {Los Angeles, California, United States}, owner = {cecile}, timestamp = {2009.11.30} } @ARTICLE{mcmillan00methodology, author = {K.L. McMillan}, title = {A {M}ethodology for {H}ardware {V}erification {U}sing {C}ompositional {M}odel {C}hecking}, journal = {Science of Computer Programming}, year = {2000}, volume = {37}, pages = {279--309}, number = {1--3}, file = {mcmillan99methodology.pdf:/dsk/l1/misc/doc/modular/assume/mcmillan99methodology.pdf:PDF}, keywords = {CTL, LTL, model checking, modular, composition, assume-guarantee}, url = {citeseer.ist.psu.edu/mcmillan99methodology.html} } @BOOK{mcmillanSMV, title = {Symbolic Model Checking}, publisher = {Kluwer Academics Publishers}, year = {1993}, author = {K.L.~McMillan} } @PHDTHESIS{memmi:thesis, author = {G.~Memmi}, title = {M\'ethodes d'analyse des r\'eseaux de Petri, r\'eseaux \`a files et application aux syst\`emes temps-r\'eel}, school = {Universit\'e Paris-6}, year = {1983} } @BOOK{Mil89, title = {Communication and {C}oncurrency}, publisher = {Prentice Hall}, year = {1989}, author = {R.~Milner}, series = {International series in computer science}, address = {Upper Saddle River, USA}, isbn = {0-13-115007-3} } @INPROCEEDINGS{DBLP:conf/ijcai/Milner71, author = {R.~Milner}, title = {{An Algebraic Definition of Simulation Between Programs.}}, booktitle = {IJCAI'71: Proceedings of the 2nd International Joint Conference on Artificial Intelligence}, year = {1971}, pages = {481-489}, adress = {London, UK}, bibsource = {DBLP, http://dblp.uni-trier.de}, editors = {D. C. Cooper}, keywords = {simulation, bisimulation} } @INPROCEEDINGS{minato, author = {S.~Minato and N.~Ishiura and S.~Yajima}, title = {Shared Binary Decision Diagrams with Attributed Edges for Efficient Boolean Function Manipulation}, booktitle = {Proceedings of the 27th ACM/IEEE Design Automation Conference, DAC'90}, year = {1990}, editor = {L.J.M Claesen}, pages = {52--57}, month = {June}, abstract = { This paper is the first one in which management of BDD nodes via a hash table is proposed (and thus the reduction operation is suppressed). Then, various labelling of edges are discussed: first, the flag $+/-$ already proposed by Billon and Madre \cite{Bil87,MB88}. Second, another flag so-called input inverter, is proposed. It transforms $ite(x,F,G)$ into $ite(\neg x,F,G)=ite(x,G,F)$. Canonicity is maintained by keeping only nodes such that $F
*Uses standard 32-bit MIPS 32 as the primary teaching ISA.
*Presents the assembler-to-HLL translations in both C and Java.
*Highlights the latest developments in architecture in Real Stuff sections:

+ Intel IA-32
+ Power PC 604
+ Googles PC cluster
+ Pentium P4
+ SPEC CPU2000 benchmark suite for processors
+ SPEC Web99 benchmark for web servers
+ EEMBC benchmark for embedded systems
+ AMD Opteron memory hierarchy
+ AMD vs. 1A-64


New support for distinct course goals

Many of the adopters who have used our book throughout its two editions are refining their courses with a greater hardware or software focus. We have provided new material to support these course goals:

New material to support a Hardware Focus

+Using logic design conventions
+Designing with hardware description languages
+Advanced pipelining
+Designing with FPGAs
+HDL simulators and tutorials
+Xilinx CAD tools

New material to support a Software Focus

+How compilers Work
+How to optimize compilers
+How to implement object oriented languages
+MIPS simulator and tutorial
+History sections on programming languages, compilers, operating systems and databases

Whats New in the Third Edition

New pedagogical features

Understanding Program Performance
-Analyzes key performance issues from the programmers perspective

Check Yourself Questions
-Helps students assess their understanding of key points of a section

Computers In the Real World
-Illustrates the diversity of applications of computing technology beyond traditional desktop and servers

For More Practice
-Provides students with additional problems they can tackle

In More Depth
-Presents new information and challenging exercises for the advanced student


New reference features

Highlighted glossary terms and definitions appear on the book page, as bold-faced entries in the index, and as a separate and searchable reference on the CD.

A complete index of the material in the book and on the CD appears in the printed index and the CD includes a fully searchable version of the same index.

Historical Perspectives and Further Readings have been updated and expanded to include the history of software R\&D.

CD-Library provides materials collected from the web which directly support the text.

On the CD

CD-Bars: Full length sections that are introduced in the book and presented on the CD

CD-Appendixes: The entire set of appendixes

CD-Library: Materials collected from the web which directly support the text

CD-Exercises: For More Practice provides exercises and solutions for self-study
In More Depth presents new information and challenging exercises for the advanced or curious student

Glossary: Terms that are defined in the text are collected in this searchable reference

Further Reading: References are organized by the chapter they support

Software: HDL simulators, MIPS simulators, and FPGA design tools

Tutorials: SPIM, Verilog, and VHDL

Additional Support: Processor Models, Labs, Homeworks, Index covering the book and CD contents

Instructor Support

+ Instructor Support is provided in a password-protected site to adopters who request the password from our sales representative
+ Solutions to all the exercises
+ Figures from the book in a number of formats
+ Lecture slides prepared by the authors and other instructors
+ Lecture notes

For instructor resources click on the grey "companion site" button found on the right side of this page.
This new edition represents a major revision.
New to this edition:

* Entire Text has been updated to reflect new technology
* 70% new exercises.
* Includes a CD loaded with software, projects and exercises to support courses using a number of tools
* A new interior design presents defined terms in the margin for quick reference
* A new feature, Understanding Program Performance focuses on performance from the programmers perspective
* Two sets of exercises and solutions, For More Practice and In More Depth, are included on the CD
* Check Yourself questions help students check their understanding of major concepts
* Computers In the Real World feature illustrates the diversity of uses for information technology
*More detail below...}}, citeulike-article-id = {808853}, howpublished = {Paperback}, isbn = {1558606041}, keywords = {pipeline,processor}, priority = {2}, url = {http://www.amazon.co.uk/exec/obidos/ASIN/1558606041/citeulike-21} } @PHDTHESIS{peng02thesis, author = {H.~Peng}, title = {Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction}, school = {Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada}, year = {2002}, owner = {cecile}, timestamp = {2007.01.09} } @ARTICLE{peng03comparison, author = {H.~Peng and S.~Tahar and F.~Khendek}, title = {Comparison of {SPIN} and {VIS} for {P}rotocol {V}erification.}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, year = {2003}, volume = {4}, pages = {234-245}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1007/s100090200073}, publisher = {Springer} } @INPROCEEDINGS{omi95rsp, author = {V. Pevtschin}, title = {The {O}pen {M}icroprocessor {S}ystems {I}nitiative: {A} {S}trategy {T}owards {I}ntegrated {S}ystem {D}esign}, booktitle = {R{SP}'95: {P}roceddings of the 6th {IEEE} {I}nternational {W}orkshop on {R}apid {S}ystem {P}rototyping}, year = {1995}, pages = {2--11}, doi = {http://doi.ieeecomputersociety.org/10.1109/IWRSP.1995.518564}, owner = {cecile}, timestamp = {2007.02.19} } @INPROCEEDINGS{plath99sfi, author = {M.C.~Plath and M.D.~Ryan}, title = {S{FI}: a {F}eature {I}ntegration {T}ool}, booktitle = {Tool Support for System Specification, Development and Verification}, year = {1999}, editor = {R. Berghammer and Y. Lakhnech}, series = {Advances in Computing Science}, pages = {201--216}, publisher = {Springer}, file = {plath99sfi.ps:/dsk/l1/misc/doc/telecom/plath99sfi.ps:PDF}, keywords = {feature} } @ARTICLE{plath01feature, author = {M.~Plath and M.~Ryan}, title = {Feature {I}ntegration using a {F}eature {C}onstruct}, journal = {Science of Computer Programming}, year = {2001}, volume = {41}, pages = {53--84}, number = {1}, address = {Amsterdam, The Netherlands}, doi = {http://dx.doi.org/10.1016/S0167-6423(00)00018-6}, issn = {0167-6423}, publisher = {Elsevier North-Holland, Inc.} } @INPROCEEDINGS{plath98feature, author = {M.C.~Plath and M.D.~Ryan}, title = {A feature construct for Promela}, booktitle = {SPIN'98: Proceedings of the 4th SPIN workshop}, year = {1998}, url = {citeseer.ist.psu.edu/plath98feature.html} } @INPROCEEDINGS{Purandare09Strengthening, author = {M. Purandare and T. Wahl and D. Kroening}, title = {Strengthening Properties Using on Refinement}, booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe}, year = {2009}, pages = {1692-1697}, file = {:Cegar/Strenghtening Properties Using AR 09.PDF:PDF}, owner = {cecile}, timestamp = {2009.04.30} } @MASTERSTHESIS{fredHDR, author = {P{\'e}trot, F.}, title = {Int{\'e}gration des syst{\`e}mes mat{\'e}riel/logiciel}, school = {Universit{\'e}e Pierre et Marie Curie}, year = {2003}, type = {Habilitation {\`a} Diriger des Recherches}, owner = {cecile}, timestamp = {2007.02.03} } @BOOK{rasiowa78algebra, title = {An Algebraic Approach to Non-Classicals Logis}, year = {1978}, editor = {Studies in Logics and the Foundations of Mathematics}, author = {H.~Rasiowa}, address = {Amsterdam}, owner = {cecile}, timestamp = {2006.05.15} } @INPROCEEDINGS{sawada97trace, author = {J.~Sawada and W.A.~Hunt}, title = {Trace {T}able {B}ased {A}pproach for {P}ipeline {M}icroprocessor {V}erification}, booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification}, year = {1997}, pages = {364--375}, address = {London, UK}, publisher = {Springer-Verlag LNCS 1254}, isbn = {3-540-63166-6} } @INPROCEEDINGS{eveking06fdl, author = {M.~Schickel and V.~Nimbler and M.~Braun and H.~Eveking}, title = {On {C}onsistency and {C}ompletness of {P}roperty-{S}ets~: {Exploiting the {P}roperty-{B}ased {D}esign {P}rocess}}, booktitle = {FDL'06: Proceeding of Forum on specification and Design Languages}, year = {2006}, keywords = {Property-based design} } @ARTICLE{DBLP:journals/fmsd/SegerB95, author = {Carl-Johan H. Seger and Randal E. Bryant}, title = {Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories}, journal = {Formal Methods in System Design}, year = {1995}, volume = {6}, pages = {147-189}, number = {2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @ARTICLE{Sharygin2012, author = {Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich}, title = {An abstraction refinement approach combining precise and approximated techniques}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, year = {2012}, volume = {14}, pages = {1-14}, file = {:/users/outil/verif/biblio/Cegar/A_framework_forCVofMVviaAR-ATVA09.pdf:PDF}, keywords = {Predicate abstraction, Precise abstraction, Approximated abstraction, CEGAR}, publisher = {Springer}, url = {http://dx.doi.org/10.1007/s10009-011-0185-y} } @INPROCEEDINGS{magnier-sherman:factotum, author = {D.J Sherman and N. Magnier}, title = {Factotum: Automatic and Systematic Sharing Support for Systems Analyzers}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98)}, year = {1982}, editor = {Bernhard Steffen}, address = {Lisbon, Portugal}, month = {March-April}, publisher = {Springer-Verlag LNCS 1384} } @INPROCEEDINGS{shoham06precision, author = {S.~Shoham and O.~Grumberg}, title = {3-Valued Abstraction: More Precision at Less Cost}, booktitle = {LICS '06: proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science}, year = {2006}, pages = {399--410}, address = {Washington, DC, USA}, publisher = {IEEE Computer Society}, doi = {http://dx.doi.org/10.1109/LICS.2006.5}, keywords = {Abstraction, 3-valued}, owner = {cecile}, timestamp = {2007.01.14} } @ARTICLE{DBLP:journals/tcad/SmithVAV05, author = {Alexander Smith and Andreas G. Veneris and Moayad Fahim Ali and Anastasios Viglas}, title = {Fault diagnosis and logic debugging using Boolean satisfiability}, journal = {IEEE Trans. on CAD of Integrated Circuits and Systems}, year = {2005}, volume = {24}, pages = {1606-1621}, number = {10}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1109/TCAD.2005.852031} } @INCOLLECTION{IMM2001-0855, author = {J. Spars{\o}}, title = {Asynchronous {C}ircuit {D}esign - {A} {T}utorial}, booktitle = {Chapters {1-}8 in {''}Principles of asynchronous circuit design - A systems Perspective''}, publisher = {Kluwer Academic Publishers}, year = {2001}, pages = {1-152}, address = {London}, month = {dec}, isbn_issn = {0-7923-7613-7}, url = {http://www2.imm.dtu.dk/pubdb/p.php?855} } @MANUAL{AtelierB, title = {{A}telier {B}, {M}anuel {U}tilisateur}, author = {{{STERIA} Technologie de l'information}}, address = {Aix-en-Provence, France}, year = {1998}, keywords = {theorem prover, b}, series = {version 3.5} } @PHDTHESIS{turk05thesis, author = {T\"urk, T.}, title = {A Hierarchy for Accellera's Property Specification Language}, school = {University of Kaiserslautern}, year = {2005}, comment = {Je l'ai en papier}, keywords = {automata approach, PSL}, owner = {cecile}, timestamp = {2006.02.13}, url = {http://thomas-tuerk.de/dokumente/Diplomarbeit.pdf} } @MANUAL{vismanual, title = {VIS User's Manual}, author = {{The VIS Group}}, year = {1996}, file = {vis_user.ps:/dsk/l1/misc/doc/checker/vis_user.ps:PDF}, key = VIS, keywords = {model checker}, owner = {cecile}, timestamp = {2006.02.09} } @INPROCEEDINGS{Tripakis201, author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye, Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang and Kormerup, Jacob and Wong, Ian}, title = {Correct and non-defensive glue design using abstract models}, booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis}, year = {2011}, series = {CODES+ISSS '11}, pages = {59--68}, address = {New York, NY, USA}, publisher = {ACM}, abstract = { Current hardware design practice often relies on integration of components, some of which may be IP or legacy blocks. While integration eases design by allowing modularization and component reuse, it is still done in a mostly ad hoc manner. Designers work with descriptions of components that are either informal or incomplete (e.g., documents in English, structural but non-behavioral specifications in IP-XACT) or too low-level (e.g., HDL code), and have little to no automatic support for stitching the components together. Providing such support is the glue design problem. This paper addresses this problem using a model-based approach. The key idea is to use high-level models, such as dataflow graphs, that enable efficient automated analysis. The analysis can be used to derive performance properties of the system (e.g., component compatibility, throughput, etc.), optimize resource usage (e.g., buffer sizes), and even synthesize low-level code (e.g., control logic). However, these models are only abstractions of the real system, and often omit critical information. As a result, the analysis outcomes may be defensive (e.g., buffers that are too big) or even incorrect (e.g., buffers that are too small). The paper examines these situations and proposes a correct and non-defensive design methodology that employs the right models to explore accurate performance and resource trade-offs. }, acmid = {2039382}, doi = {http://doi.acm.org/10.1145/2039370.2039382}, isbn = {978-1-4503-0715-4}, keywords = {abstraction, data flow, glue design, non-defensiveness, composition}, location = {Taipei, Taiwan}, numpages = {10}, owner = {cecile}, timestamp = {2012.03.07}, url = {http://doi.acm.org/10.1145/2039370.2039382} } @MISC{m106archi, author = {{Universit\'e Pierre et Marie Curie (UPMC), Paris 6}}, title = {{{UE} : Achitecture des syst\`emes int\'egr\'es, {M1}}}, note = {\url{http://www-master.ufr-info-p6.jussieu.fr/ue/archi/}}, owner = {cecile}, timestamp = {2006.10.05} } @ARTICLE{fms, author = {D.M.~Upton}, title = {A {F}lexible {S}tructure for {C}omputer-{C}ontrolled {M}anufacturing {S}ystems}, journal = {Manufacturing Review}, year = {1992}, volume = {5}, pages = {58--74}, number = {1}, keywords = {FMS}, owner = {cecile}, timestamp = {2007.01.22} } @INPROCEEDINGS{Valk93, author = {R. Valk}, title = {Bridging the Gap between Place- and Floyd-Invariants with Applications to Preemptive Scheduling}, booktitle = {Proc. of ICATPN'93}, year = {1993}, volume = {691}, series = {Lecture Notes in Computer Science}, pages = {432--452}, publisher = {Springer Verlag} } @INPROCEEDINGS{xie03verified, author = {F.~Xie and J.C.~Browne}, title = {Verified {S}ystems by {C}omposition from {V}erified {C}omponents}, booktitle = {E{SEC}/{FSE} 2003 : {P}roceedings of the 11th {ACM} {SIGSOFT} {S}ymposium on {F}oundations of {S}oftware {E}ngineering 2003 held jointly with 9th {E}uropean {S}oftware {E}ngineering {C}onference}, year = {2003}, pages = {277--286}, address = {Helsinki, Finland}, publisher = {ACM Press}, comment = {: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering}, doi = {http://doi.acm.org/10.1145/940071.940109}, isbn = {1-58113-743-5}, location = {Helsinki, Finland} } @PHDTHESIS{Yadgar10thesis, author = {Avi Yadgar}, title = {New Approaches to Model Checking and to 3-Valued Abstraction and Refinement}, school = {Technion - Israel Institute of Technology}, year = {2010}, file = {:/users/outil/verif/biblio/Cegar/AviYadgarPhDThesisReport.pdf:PDF}, keywords = {Cegar, BMC, 3-valued, Abstraction}, owner = {verif}, timestamp = {2010.06.15} } @TECHREPORT{cegarhwcasestudy07, author = {Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah}, title = {CEGAR-Based Formal Hardware Verification: A Case Study}, institution = {Department of Electrical Engineering and Computer Science University of Michigan}, year = {2007}, file = {:Cegar/CEGARHWVerifCaseStudy07.pdf:PDF}, keywords = {CEGAR,hardware}, owner = {cecile}, timestamp = {2010.06.10} } @ARTICLE{Zaki08analogformalsurvey, author = {M.H~Zaki and S.~Tahar and G.~Bois}, title = {Formal verification of analog and mixed signal designs: A survey}, journal = {Microelectronics Journal}, year = {2008}, volume = {39}, pages = {1395--1404}, number = {12}, address = {Amsterdam, The Netherlands, The Netherlands}, doi = {http://dx.doi.org/10.1016/j.mejo.2008.05.013}, file = {:Analog/surveyZaki08.pdf:PDF}, issn = {0026-2692}, publisher = {Elsevier Science Publishers B. V.} } @ARTICLE{5374376, author = {Hao Zheng and Haiqiong Yao and Yoneda, T.}, title = {Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement}, journal = {Computers, IEEE Transactions on}, year = {2010}, volume = {59}, pages = {561 -573}, number = {4}, month = {april }, abstract = {Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements.}, doi = {10.1109/TC.2009.187}, file = {:/users/outil/verif/biblio/Composition/ModularMCLargeAsynchronousDesignwithAR2010.pdf:PDF}, issn = {0018-9340}, keywords = {abstraction refinement;abstraction refinement method;large asynchronous designs;modular model checking;state explosion;state space reduction techniques;formal verification;state-space methods; composition}, owner = {cecile}, review = {Verification of a whole system by verifying each components. When verifying each components individually assumptions has to be made on the environnment ot avoid false counter-examples. Use component abstraction to over-approximated the environment. This abastraction must be refined to obtain only the behavior allowed at the interface. They propose : Main contribution : Local synchronization detection method for component based on parallel composition and an AR methof for modular MC.
Circuit class : Asynchronous}, timestamp = {2012.03.07} } @PROCEEDINGS{DBLP:conf/fmcad/2002, title = {Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings}, year = {2002}, editor = {Mark Aagaard and John W. O'Leary}, volume = {2517}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {FMCAD}, isbn = {3-540-00116-6} } @PROCEEDINGS{DBLP:conf/sefm/2005, title = {Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany}, year = {2005}, editor = {Bernhard K. Aichernig and Bernhard Beckert}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {SEFM}, isbn = {0-7695-2435-4} } @PROCEEDINGS{DBLP:conf/cav/2004, title = {Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings}, year = {2004}, editor = {Rajeev Alur and Doron Peled}, volume = {3114}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-22342-8} } @PROCEEDINGS{DBLP:conf/cav/2006, title = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification}, year = {2006}, editor = {Thomas Ball and Robert B. Jones}, volume = {4144}, series = {Lecture Notes in Computer Science}, address = {Seattle, WA, USA}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-37406-X} } @PROCEEDINGS{DBLP:conf/sfm/2006, title = {Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures}, year = {2006}, editor = {Marco Bernardo and Alessandro Cimatti}, volume = {3965}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {SFM}, isbn = {978-3-540-34304-2} } @PROCEEDINGS{DBLP:conf/cav/2001, title = {Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings}, year = {2001}, editor = {G{\'e}rard Berry and Hubert Comon and Alain Finkel}, volume = {2102}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-42345-1} } @PROCEEDINGS{DBLP:conf/hvc/2006, title = {Hardware and Software, Verification and Testing, Second International Haifa Verification Conference, HVC 2006, Haifa, Israel, October 23-26, 2006. Revised Selected Papers}, year = {2007}, editor = {Eyal Bin and Avi Ziv and Shmuel Ur}, volume = {4383}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {Haifa Verification Conference}, isbn = {978-3-540-70888-9} } @PROCEEDINGS{DBLP:conf/fmco/2005, title = {Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures}, year = {2006}, editor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever}, volume = {4111}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {FMCO}, isbn = {3-540-36749-7} } @PROCEEDINGS{DBLP:conf/charme/2005, title = {Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbr{\"u}cken, Germany, October 3-6, 2005, Proceedings}, year = {2005}, editor = {Dominique Borrione and Wolfgang J. Paul}, volume = {3725}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CHARME}, isbn = {3-540-29105-9}, owner = {cecile}, timestamp = {2006.06.27} } @PROCEEDINGS{DBLP:conf/cav/2002, title = {Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings}, year = {2002}, editor = {Ed Brinksma and Kim Guldstrand Larsen}, volume = {2404}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-43997-8} } @PROCEEDINGS{DBLP:conf/fase/2005, title = {Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings}, year = {2005}, editor = {Maura Cerioli}, volume = {3442}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {FASE}, isbn = {3-540-25420-X} } @PROCEEDINGS{DBLP:conf/lpar/2008, title = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings}, year = {2008}, editor = {Iliano Cervesato and Helmut Veith and Andrei Voronkov}, volume = {5330}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {LPAR}, isbn = {978-3-540-89438-4} } @PROCEEDINGS{DBLP:conf/vmcai/2005, title = {Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings}, year = {2005}, editor = {Radhia Cousot}, volume = {3385}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {VMCAI}, isbn = {3-540-24297-X} } @PROCEEDINGS{DBLP:conf/tcs/1981, title = {Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings}, year = {1981}, editor = {Peter Deussen}, volume = {104}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {Theoretical Computer Science}, isbn = {3-540-10576-X} } @PROCEEDINGS{DBLP:conf/vmcai/2006, title = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings}, year = {2006}, editor = {E. Allen Emerson and Kedar S. Namjoshi}, volume = {3855}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {VMCAI}, isbn = {3-540-31139-4} } @PROCEEDINGS{DBLP:conf/cav/2000, title = {Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings}, year = {2000}, editor = {E.A.~Emerson and A.P.~Sistla}, volume = {1855}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-67770-4}, owner = {cecile}, timestamp = {2006.02.13} } @PROCEEDINGS{DBLP:conf/apn/2002, title = {Applications and Theory of Petri Nets 2002, 23rd International Conference, ICATPN 2002, Adelaide, Australia, June 24-30, 2002, Proceedings}, year = {2002}, editor = {Javier Esparza and Charles Lakos}, volume = {2360}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {ICATPN}, isbn = {3-540-43787-8} } @PROCEEDINGS{DBLP:conf/date/2006p, title = {Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2006, Munich, Germany, March 6-10, 2006}, year = {2006}, editor = {Georges G. E. Gielen}, publisher = {European Design and Automation Association, Leuven, Belgium}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DATE}, isbn = {3-9810801-0-6} } @PROCEEDINGS{DBLP:conf/sat/2003, title = {Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers}, year = {2004}, editor = {Enrico Giunchiglia and Armando Tacchella}, volume = {2919}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {SAT}, isbn = {3-540-20851-8} } @PROCEEDINGS{DBLP:conf/frocos/2005, title = {Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings}, year = {2005}, editor = {Bernhard Gramlich}, volume = {3717}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {FroCoS}, isbn = {3-540-29051-6} } @PROCEEDINGS{DBLP:conf/cav/1997, title = {Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings}, year = {1997}, editor = {Orna Grumberg}, volume = {1254}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-63166-6} } @PROCEEDINGS{DBLP:conf/cav/1999, title = {Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings}, year = {1999}, editor = {Nicolas Halbwachs and Doron Peled}, volume = {1633}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-66202-2}, owner = {cecile}, timestamp = {2006.04.25} } @PROCEEDINGS{DBLP:conf/tacas/2005, title = {Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings}, year = {2005}, editor = {Nicolas Halbwachs and Lenore D. Zuck}, volume = {3440}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TACAS}, isbn = {3-540-25333-5} } @PROCEEDINGS{DBLP:conf/iccad/2006, title = {2006 International Conference on Computer-Aided Design (ICCAD'06), November 5-9, 2006, San Jose, CA, USA}, year = {2006}, editor = {Soha Hassoun}, publisher = {ACM}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {ICCAD}, isbn = {1-59593-389-1} } @PROCEEDINGS{DBLP:conf/tacas/2006, title = {Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings}, year = {2006}, editor = {Holger Hermanns and Jens Palsberg}, volume = {3920}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TACAS}, isbn = {3-540-33056-9} } @PROCEEDINGS{DBLP:conf/cav/1998, title = {Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings}, year = {1998}, editor = {Alan J. Hu and Moshe Y. Vardi}, volume = {1427}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-64608-6} } @PROCEEDINGS{DBLP:conf/tacas/2004, title = {Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings}, year = {2004}, editor = {Kurt Jensen and Andreas Podelski}, volume = {2988}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TACAS}, isbn = {3-540-21299-X} } @PROCEEDINGS{DBLP:conf/vmcai/2011, title = {Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings}, year = {2011}, editor = {Ranjit Jhala and David A. Schmidt}, volume = {6538}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {VMCAI}, ee = {http://dx.doi.org/10.1007/978-3-642-18275-4}, isbn = {978-3-642-18274-7} } @PROCEEDINGS{DBLP:conf/cav/2003, title = {Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings}, year = {2003}, editor = {Warren A. Hunt Jr. and Fabio Somenzi}, volume = {2725}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CAV}, isbn = {3-540-40524-0} } @PROCEEDINGS{DBLP:conf/dac/2005, title = {Proceedings of the 42nd Design Automation Conference, DAC 2005, San Diego, CA, USA, June 13-17, 2005}, year = {2005}, editor = {William H. Joyner Jr. and Grant Martin and Andrew B. Kahng}, publisher = {ACM}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DAC}, isbn = {1-59593-058-2} } @PROCEEDINGS{DBLP:conf/lop/1981, title = {Logic of Programs, Workshop}, year = {1982}, editor = {Dexter Kozen}, volume = {131}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {Logic of Programs}, isbn = {3-540-11212-X} } @PROCEEDINGS{DBLP:conf/dac/2004, title = {Proceedings of the 41th Design Automation Conference, DAC 2004, San Diego, CA, USA, June 7-11, 2004}, year = {2004}, editor = {Sharad Malik and Limor Fix and Andrew B. Kahng}, publisher = {ACM}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DAC}, isbn = {1-58113-828-8} } @PROCEEDINGS{DBLP:conf/birthday/2010pnueli, title = {Time for Verification, Essays in Memory of Amir Pnueli}, year = {2010}, editor = {Zohar Manna and Doron Peled}, volume = {6200}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {Essays in Memory of Amir Pnueli}, ee = {http://dx.doi.org/10.1007/978-3-642-13754-9}, isbn = {978-3-642-13753-2} } @PROCEEDINGS{DBLP:conf/tacas/2001, title = {Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings}, year = {2001}, editor = {Tiziana Margaria and Wang Yi}, volume = {2031}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TACAS}, isbn = {3-540-41865-2} } @PROCEEDINGS{DBLP:conf/sbmf/2009, title = {Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers}, year = {2009}, editor = {Marcel Vinicius Medeiros Oliveira and Jim Woodcock}, volume = {5902}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {SBMF}, ee = {http://dx.doi.org/10.1007/978-3-642-10452-7}, isbn = {978-3-642-10451-0} } @PROCEEDINGS{DBLP:conf/concur/2000, title = {CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings}, year = {2000}, editor = {Catuscia Palamidessi}, volume = {1877}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {CONCUR}, isbn = {3-540-67897-2} } @PROCEEDINGS{DBLP:conf/tacas/2008, title = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings}, year = {2008}, editor = {C. R. Ramakrishnan and Jakob Rehof}, volume = {4963}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TACAS}, isbn = {978-3-540-78799-0} } @PROCEEDINGS{DBLP:conf/compos/1997, title = {Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures}, year = {1998}, editor = {Willem P. de Roever and Hans Langmaack and Amir Pnueli}, volume = {1536}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {COMPOS}, isbn = {3-540-65493-3} } @PROCEEDINGS{DBLP:conf/dac/2006, title = {Proceedings of the 43rd Design Automation Conference, DAC 2006, San Francisco, CA, USA, July 24-28, 2006}, year = {2006}, editor = {Ellen Sentovich}, publisher = {ACM}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DAC}, isbn = {1-59593-381-6} } @PROCEEDINGS{DBLP:conf/tacas/1998, title = {Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings}, year = {1998}, editor = {Bernhard Steffen}, volume = {1384}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TACAS}, isbn = {3-540-64356-7} } @PROCEEDINGS{DBLP:conf/forte/2005, title = {Formal Techniques for Networked and Distributed Systems - FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings}, year = {2005}, editor = {Farn Wang}, volume = {3731}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {FORTE}, isbn = {3-540-29189-X} } @PROCEEDINGS{DBLP:conf/fm/1999-1, title = {FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I}, year = {1999}, editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, volume = {1708}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {World Congress on Formal Methods}, isbn = {3-540-66587-0} } @MISC{alliance, title = {Alliance, a free {VLSI} cad system}, note = {\\\url{http://www-asim.lip6.fr/recherche/alliance/}}, owner = {cecile}, timestamp = {2007.02.01} } @MISC{onespin, title = {OneSpin Solutions}, note = {\url{http://www.onespin-solutions.com/}}, key = OneS, owner = {cecile}, timestamp = {2007.03.07} } @MISC{prosyd, title = {The Prosyd Project on Property-Based System Design}, note = {{\url{http://www.prosyd.org/}}}, owner = {cecile}, timestamp = {2007.02.07} } @MISC{soclib, title = {The {S}o{CL}ib {P}roject}, note = {\url{http://soclib.lip6.fr/}}, key = SoC, owner = {cecile}, timestamp = {2006.09.07}, url = {http://soclib.lip6.fr/} } @MISC{texas97bench, title = {Texas-97 {V}erification {B}enchmarks}, note = {\\\url{http://www.cad.eecs.berkeley.edu/Respep/Research/vis/texas-97/}}, key = TEXAS, keywords = {protocol, PIbus}, owner = {cecile}, timestamp = {2006.11.30} } @MISC{vsia, title = {{VSI A}lliance}, note = {\url{http://www.vsi.org/}}, key = VSI, owner = {cecile}, timestamp = {2006.09.13} } @PROCEEDINGS{DBLP:conf/date/2009, title = {Design, Automation and Test in Europe, DATE 2009, Nice, France, April 20-24, 2009}, year = {2009}, publisher = {IEEE}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DATE} } @PROCEEDINGS{DBLP:conf/fmcad/2009, title = {Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA}, year = {2009}, publisher = {IEEE}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {FMCAD}, isbn = {978-1-4244-4966-8} } @PROCEEDINGS{DBLP:conf/lics/2004, title = {19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings}, year = {2004}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {LICS}, isbn = {0-7695-2192-4} } @PROCEEDINGS{DBLP:conf/sat/2004, title = {SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings}, year = {2004}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {SAT}, owner = {cecile}, timestamp = {2009.01.27} } @PROCEEDINGS{DBLP:conf/date/2003, title = {2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany}, year = {2003}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DATE}, isbn = {0-7695-1870-2} } @PROCEEDINGS{DBLP:conf/icse/2003, title = {Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA}, year = {2003}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {ICSE} } @PROCEEDINGS{DBLP:conf/time/2003, title = {10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), 8-10 July 2003, Cairns, Queensland, Australia}, year = {2003}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {TIME}, isbn = {0-7695-1912-1} } @PROCEEDINGS{DBLP:conf/iccd/2002, title = {20th International Conference on Computer Design (ICCD 2002), VLSI in Computers and Processors, 16-18 September 2002, Freiburg, Germany, Proceedings}, year = {2002}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {ICCD}, isbn = {0-7695-1700-5}, keywords = {3-valued, logic, model checking, Kripke structure} } @PROCEEDINGS{DBLP:conf/dac/2001, title = {Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001}, year = {2001}, publisher = {ACM}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {DAC}, isbn = {1-58113-297-2} } @PROCEEDINGS{DBLP:conf/icse/2001, title = {Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, 12-19 May 2001, Toronto, Ontario, Canada}, year = {2001}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {ICSE}, isbn = {0-7695-1050-7} } @MANUAL{amba, title = {AMBA Specification}, organization = {ARM limited}, edition = {2.0}, year = {1999}, note = {ARM Limited \copyright. All right reserved}, file = {IHI0011A_AMBA_SPEC.pdf:/dsk/l1/misc/doc/amba/IHI0011A_AMBA_SPEC.pdf:PDF}, key = AMBA, owner = {cecile}, timestamp = {2006.09.07} } @MANUAL{formalcheck, title = {Formal Verification Using Affirma {FormalCheck}}, organization = {Cadence}, month = {October}, year = {1999} } @PROCEEDINGS{DBLP:conf/lics/LICS4, title = {Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA}, year = {1989}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {LICS} } @PROCEEDINGS{DBLP:conf/lics/LICS3, title = {Proceedings, Third Annual Symposium on Logic in Computer Science}, year = {1988}, address = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {LICS} } @PROCEEDINGS{DBLP:conf/stoc/STOC14, title = {Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, 5-7 May 1982, San Francisco, California, USA}, year = {1982}, publisher = {ACM}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {STOC} }