ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Digital Library logoTake a look at the new version of this page: [ beta version ]. Tell us what you think.
Symbolic Model Checking
Symbolic Model Checking
  Purchase this Book  
Source
Pages: 216  
Medium: Hardcover
Year of Publication: 1993
ISBN:0792393805
Author
Kenneth L. McMillan
Publisher
Kluwer Academic Publishers  Norwell, MA, USA
Bibliometrics
Downloads (6 Weeks): n/a,   Downloads (12 Months): n/a,   Citation Count: 474
Additional Information:

cited by   collaborative colleagues  

Tools and Actions: Review this Book  

CITED BY  474
Malay K. Ganai , Weihong Li, Bang for the buck: improvising and scheduling verification engines for effective resource utilization, Proceedings of the 7th IEEE/ACM international conference on Formal Methods and Models for Codesign, p.8-17, July 13-15, 2009, Cambridge, Massachusetts
Subir K. Roy , Hiroaki Iwashita , Tsuneo Nakata, Formal verification based on assume and guarantee approach — a case study (short paper), Proceedings of the 2000 conference on Asia South Pacific design automation, p.77-80, January 2000, Yokohama, Japan
Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996
Michael Kishinevsky , Jordi Cortadella , Alex Kondratyev, Asynchronous interface specification, analysis and synthesis, Proceedings of the 35th annual conference on Design automation, p.2-7, June 15-19, 1998, San Francisco, California, United States
Rajnish Ghughal , Abdel Mokkedem , Ratan Nalumasu , Ganesh Gopalakrishnan, Using “test model-checking” to verify the Runway-PA8000 memory model, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.231-239, June 28-July 02, 1998, Puerto Vallarta, Mexico
Karen Yorav , Orna Grumberg, Static Analysis for State-Space Reductions Preserving Temporal Logics, Formal Methods in System Design, v.25 n.1, p.67-96, July 2004
Adnan Aziz , Jim Kukula , Tom Shiple, Hybrid verification using saturated simulation, Proceedings of the 35th annual conference on Design automation, p.615-618, June 15-19, 1998, San Francisco, California, United States
Scott Hazelhurst , Osnat Weissberg , Gila Kamhi , Limor Fix, A hybrid verification approach: getting deep into the design, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
K. L. McMillan, Fitting formal methods into the design cycle, Proceedings of the 31st annual conference on Design automation, p.314-319, June 06-10, 1994, San Diego, California, United States
Cindy Eisner , Irit Shitsevalov , Russ Hoover , Wayne Nation , Kyle Nelson , Ken Valk, A methodology for formal design of hardware control with application to cache coherence protocols, Proceedings of the 37th conference on Design automation, p.724-729, June 05-09, 2000, Los Angeles, California, United States
Paolo Baldan , Andrea Corradini , Ugo Montanari, Contextual Petri nets, asymmetric event structures, and processes, Information and Computation, v.171 n.1, p.1-49, November 25, 2001
G. J. Holzmann , R. Joshi , A. Groce, Swarm Verification, Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, p.1-6, September 15-19, 2008
Jae-Young Jang , In-Ho Moon , Gary D. Hachtel, Iterative abstraction-based CTL model checking, Proceedings of the conference on Design, automation and test in Europe, p.502-509, March 27-30, 2000, Paris, France
Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.156-166, Nov. 1996
Shing Chi Cheung , Jeff Kramer, Checking safety properties using compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.1, p.49-78, Jan. 1999
R. Reetz , K. Schneider , T. Kropf, Formal specification in VHDL for hardware verification, Proceedings of the conference on Design, automation and test in Europe, p.257-265, February 23-26, 1998, Le Palais des Congrés de Paris, France
Aiguo Xie , Peter A. Beerel, Efficient state classification of finite state Markov chains, Proceedings of the 35th annual conference on Design automation, p.605-610, June 15-19, 1998, San Francisco, California, United States
Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999
M. Lajolo , L. Lavagno , M. Rebaudengo , M. Sonza Reorda , M. Violante, Automatic test bench generation for simulation-based validation, Proceedings of the eighth international workshop on Hardware/software codesign, p.136-140, May 2000, San Diego, California, United States
Adnan Aziz , Felice Balarin , Robert Brayton , Alberto Sangiovanni-Vincentelli, Sequential synthesis using S1S, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.612-617, November 05-09, 1995, San Jose, California, United States
Steve Easterbrook , Marsha Chechik, A framework for multi-valued reasoning over inconsistent viewpoints, Proceedings of the 23rd International Conference on Software Engineering, p.411-420, May 12-19, 2001, Toronto, Ontario, Canada
Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000
L. Thiele , K. Strehl , D. Ziegenbein , R. Ernst , J. Teich, FunState—an internal design representation for codesign, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.558-565, November 07-11, 1999, San Jose, California, United States
Gleb Naumovich , George S. Avrunin , Lori A. Clarke, Data flow analysis for checking properties of concurrent Java programs, Proceedings of the 21st international conference on Software engineering, p.399-410, May 16-22, 1999, Los Angeles, California, United States
R. Alur , R. K. Brayton , T. A. Henzinger , S. Qadeer , S. K. Rajamani, Partial-Order Reduction in Symbolic State-Space Exploration, Formal Methods in System Design, v.18 n.2, p.97-116, March 1, 2001
Yunja Choi , Sanjai Rayadurgam , Mats P.E. Heimdahl, Automatic abstraction for model checking software systems with interrelated numeric constraints, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
William Chan , Richard J. Anderson , Paul Beame , David H. Jones , David Notkin , William E. Warner, Decoupling synchronization from local control for efficient symbolic model checking of statecharts, Proceedings of the 21st international conference on Software engineering, p.142-151, May 16-22, 1999, Los Angeles, California, United States
Hong Liu , David P. Gluch, A proposal for introducing model checking into an undergraduate software engineering curriculum, Journal of Computing Sciences in Colleges, v.18 n.2, p.259-270, December 2002
J. Ruf , D. Hoffmann , T. Kropf , W. Rosenstiel, Simulation-guided property checking based on a multi-valued AR-automata, Proceedings of the conference on Design, automation and test in Europe, p.742-748, March 2001, Munich, Germany
Ronald Herrmann , Thomas Reielts, Verification of a production cell using an automatic verification environment for VHDL, Proceedings of the conference on European design automation, p.542-547, September 18-22, 1995, Brighton, England
Pei-Hsin Ho , Adrian J. Isles , Timothy Kam, Formal verification of pipeline control using controlled token nets and abstract interpretation, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.529-536, November 08-12, 1998, San Jose, California, United States
Dirk Wodtke , Jeanine Weissenfels , Gerhard Weikum , Angelika Kotz Dittrich , Peter Muth, The MENTOR workbench for enterprise-wide workflow management, ACM SIGMOD Record, v.26 n.2, p.576-579, June 1997
Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France
Zheng Zhou , Wayne Burleson, Equivalence checking of datapaths based on canonical arithmetic expressions, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.546-551, June 12-16, 1995, San Francisco, California, United States
Yih-Chih Chou , Youn-Long Lin, A 3-step approach for performance-driven whole-chip routing, Proceedings of the 2001 conference on Asia South Pacific design automation, p.187-191, January 2001, Yokohama, Japan
Ilan Beer , Shoham Ben-David , Cindy Eisner , Avner Landver, RuleBase: an industry-oriented formal verification tool, Proceedings of the 33rd annual conference on Design automation, p.655-660, June 03-07, 1996, Las Vegas, Nevada, United States
A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States
Kathi Fisler , Shriram Krishnamurthi, Modular verification of collaboration-based software designs, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
Alexei Semenov , Alexandre Yakovlev, Verification of asynchronous circuits using time Petri net unfolding, Proceedings of the 33rd annual conference on Design automation, p.59-62, June 03-07, 1996, Las Vegas, Nevada, United States
Dong Wang , Pei-Hsin Jiang , James Kukula , Yunshan Zhu , Tony Ma , Robert Damiano, Formal property verification by abstraction refinement with formal, simulation and hybrid engines, Proceedings of the 38th conference on Design automation, p.35-40, June 2001, Las Vegas, Nevada, United States
Rajeev Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.390-402, January 19-21, 2000, Boston, MA, USA
Rik Eshuis , Roel Wieringa, Verification support for workflow design with UML activity graphs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
Xudong He , Junhua Ding , Yi Deng, Model checking software architecture specifications in SAM, Proceedings of the 14th international conference on Software engineering and knowledge engineering, July 15-19, 2002, Ischia, Italy
E. M. Clarke , M. Khaira , X. Zhao, Word level model checking—avoiding the Pentium FDIV error, Proceedings of the 33rd annual conference on Design automation, p.645-648, June 03-07, 1996, Las Vegas, Nevada, United States
Jörg Bormann , Jörg Lohse , Michael Payer , Gerd Venzl, Model checking in industrial hardware design, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.298-303, June 12-16, 1995, San Francisco, California, United States
Julia Dushina , Mike Benjamin , Daniel Geist, Semi-formal test generation with genevieve, Proceedings of the 38th conference on Design automation, p.617-622, June 2001, Las Vegas, Nevada, United States
R. P. Kurshan, Formal verification in a commercial setting, Proceedings of the 34th annual conference on Design automation, p.258-262, June 09-13, 1997, Anaheim, California, United States
Yatin Hoskote , Timothy Kam , Pei-Hsin Ho , Xudong Zhao, Coverage estimation for symbolic model checking, Proceedings of the 36th ACM/IEEE conference on Design automation, p.300-305, June 21-25, 1999, New Orleans, Louisiana, United States
James C. Corbett , Matthew B. Dwyer , John Hatcliff , Roby, Bandera: a source-level interface for model checking Java programs, Proceedings of the 22nd international conference on Software engineering, p.762-765, June 04-11, 2000, Limerick, Ireland
Shmuel Ur , Yaov Yadin, Micro architecture coverage directed generation of test programs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.175-180, June 21-25, 1999, New Orleans, Louisiana, United States
In-Ho Moon , James H. Kukula , Kavita Ravi , Fabio Somenzi, To split or to conjoin: the question in image computation, Proceedings of the 37th conference on Design automation, p.23-28, June 05-09, 2000, Los Angeles, California, United States
James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland
Roderick Bloem , Kavita Ravi , Fabio Somenzi, Symbolic guided search for CTL model checking, Proceedings of the 37th conference on Design automation, p.29-34, June 05-09, 2000, Los Angeles, California, United States
Jamieson M. Cobleigh , Lori A. Clarke , Leon J. Osterweil, The right algorithm at the right time: comparing data flow analysis algorithms for finite state verification, Proceedings of the 23rd International Conference on Software Engineering, p.37-46, May 12-19, 2001, Toronto, Ontario, Canada
S. Vercauteren , D. Verkest , G. de Jong , B. Lin, Efficient verification using generalized partial order analysis, Proceedings of the conference on Design, automation and test in Europe, p.782-789, February 23-26, 1998, Le Palais des Congrés de Paris, France
A. Semenov , A. Yakovlev , E. Pastor , M. A. Peña , J. Cortadella, Synthesis of speed-independent circuits from STG-unfolding segment, Proceedings of the 34th annual conference on Design automation, p.16-21, June 09-13, 1997, Anaheim, California, United States
R. P. Kurshan, The complexity of verification, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.365-371, May 23-25, 1994, Montreal, Quebec, Canada
David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States
Walter Hartong , Lars Hedrich , Erich Barke, Model checking algorithms for analog verification, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
William Chan , Richard J. Anderson , Paul Beame , David Notkin, Improving efficiency of symbolic model checking for state-based system requirements, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.102-112, March 1998
Thomas Ball , Sriram K. Rajamani, Bebop: a path-sensitive interprocedural dataflow engine, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.97-103, June 2001, Snowbird, Utah, United States
Chung-Yang Huang , Kwang-Ting Cheng, Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques, Proceedings of the 37th conference on Design automation, p.118-123, June 05-09, 2000, Los Angeles, California, United States
Harry Hsieh , Felice Balarin, Synchronous equivalence for embedded systems: a tool for design exploration, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.505-510, November 07-11, 1999, San Jose, California, United States
Jörg Walter , Jens Leenstra , Gerhard Döttling , Bernd Leppla , Hans-Jürgen Münster , Kevin Kark , Bruce Wile, Hierarchical random simulation approach for the verification of S/390 CMOS multiprocessors, Proceedings of the 34th annual conference on Design automation, p.89-94, June 09-13, 1997, Anaheim, California, United States
Abelardo Pardo , Gary D. Hachtel, Incremental CTL model checking using BDD subsetting, Proceedings of the 35th annual conference on Design automation, p.457-462, June 15-19, 1998, San Francisco, California, United States
Yuan Lu , Jawahar Jain , Edmund Clarke , Masahiro Fujita, Efficient variable ordering using aBDD based sampling, Proceedings of the 37th conference on Design automation, p.687-692, June 05-09, 2000, Los Angeles, California, United States
Naoyasu Ubayashi , Tetsuo Tamai, Aspect-oriented programming with model checking, Proceedings of the 1st international conference on Aspect-oriented software development, April 22-26, 2002, Enschede, The Netherlands
Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, ACM SIGPLAN Notices, v.33 n.5, p.345-357, May 1998
Tevfik Bultan, Action Language: a specification language for model checking reactive systems, Proceedings of the 22nd international conference on Software engineering, p.335-344, June 04-11, 2000, Limerick, Ireland
Hiroaki Iwashita , Tsuneo Nakata, Forward model checking techniques oriented to buggy designs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.400-404, November 09-13, 1997, San Jose, California, United States
Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.146-162, Nov. 1999
Yael Abarbanel-Vinov , Neta Aizenbud-Reshef , Ilan Beer , Cindy Eisner , Daniel Geist , Tamir Heyman , Iris Reuveni , Eran Rippel , Irit Shitsevalov , Yaron Wolfsthal , Tali Yatzkar-Haham, On the Effective Deployment of Functional Formal Verification, Formal Methods in System Design, v.19 n.1, p.35-44, July 2001
Christoph Meinel , Christian Stangier, Speeding up symbolic model checking by accelerating dynamic variable reordering, Proceedings of the 10th Great Lakes symposium on VLSI, p.39-42, March 02-04, 2000, Chicago, Illinois, United States
Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.124-133, March 1998
Tevfik Bultan , Richard Gerber , William Pugh, Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.747-789, July 1999
Shuo Sheng , Koichiro Takayama , Michael S. Hsiao, Effective safety property checking using simulation-based sequential ATPG, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Kyle L. Nelson , Alok Jain , Randal E. Bryant, Formal verification of a superscalar execution unit, Proceedings of the 34th annual conference on Design automation, p.161-166, June 09-13, 1997, Anaheim, California, United States
Y.-W. Hsieh , S. P. Levitan, Model abstraction for formal verification, Proceedings of the conference on Design, automation and test in Europe, p.140-147, February 23-26, 1998, Le Palais des Congrés de Paris, France
James C. Corbett, An empirical evaluation of three methods for deadlock analysis of Ada tasking programs, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.204-215, August 17-19, 1994, Seattle, Washington, United States
Gila Kamhi , Limor Fix, Adaptive variable reordering for symbolic model checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.359-365, November 08-12, 1998, San Jose, California, United States
James C. Corbett, Using shape analysis to reduce finite-state models of concurrent Java programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.51-93, Jan. 2000
Malay K. Ganai , Adnan Aziz , Andreas Kuehlmann, Enhancing simulation with BDDs and ATPG, Proceedings of the 36th ACM/IEEE conference on Design automation, p.385-390, June 21-25, 1999, New Orleans, Louisiana, United States
Randal E. Bryant , Christoph Meinel, Ordered binary decision diagrams, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
Dominik Stoffel , Wolfgang Kunz, Record & play: a structural fixed point iteration for sequential circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.394-399, November 09-13, 1997, San Jose, California, United States
Hiroaki Iwashita , Tsuneo Nakata , Fumiyasu Hirose, CTL model checking based on forward state traversal, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.82-87, November 10-14, 1996, San Jose, California, United States
Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
Praveen Yalagandula , Vigyan Singhal , Adnan Aziz, Automatic lighthouse generation for directed state space search, Proceedings of the conference on Design, automation and test in Europe, p.237-242, March 27-30, 2000, Paris, France
Georg Gottlob , Erich Grädel , Helmut Veith, Datalog LITE: a deductive query language with linear time model checking, ACM Transactions on Computational Logic (TOCL), v.3 n.1, p.42-79, January 2002
In-Ho Moon , James Kukula , Tom Shiple , Fabio Somenzi, Least fixpoint approximations for reachability analysis, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.41-44, November 07-11, 1999, San Jose, California, United States
Jamieson M. Cobleigh , Lori A. Clark , Leon J. Osterweil, Verifying properties of process definitions, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.96-101, Sept. 2000
Guoping Jia , Susanne Graf, Verification experiments on the MASCARA protocol, Proceedings of the 8th international SPIN workshop on Model checking of software, p.123-142, May 2001, Toronto, Ontario, Canada
Riccardo Forth , Paul Molitor, An efficient heuristic for state encoding minimizing the BDD representations of the transistion relations of finite state machines, Proceedings of the 2000 conference on Asia South Pacific design automation, p.61-66, January 2000, Yokohama, Japan
Stephen Edwards , Luciano Lavagno , Edward A. Lee , Alberto Sangiovanni-Vincentelli, Design of embedded systems: formal models, validation, and synthesis, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
Ronald Herrmann , Hergen Pargmann, Computing binary decision diagrams for VHDL data types, Proceedings of the conference on European design automation, p.578-583, September 19-23, 1994, Grenoble, France
David Wagner , Paolo Soto, Mimicry attacks on host-based intrusion detection systems, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA
Sergey Berezin , Edmund Clarke , Armin Biere , Yunshan Zhu, Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function, Formal Methods in System Design, v.20 n.2, p.159-186, March 2002
Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists, Formal Methods in System Design, v.23 n.1, p.39-65, July 2003
Teodor Rus , Eric Van Wyk , Tom Halverson, Generating Model Checkers from Algebraic Specifications, Formal Methods in System Design, v.20 n.3, p.249-284, May 2002
Satish Chandra , Patrice Godefroid , Christopher Palm, Software model checking in practice: an industrial case study, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
Warren A. Hunt, Jr. , Jun Sawada, Verifying the FM9801 Microarchitecture, IEEE Micro, v.19 n.3, p.47-55, May 1999
Marsha Chechik , Hai Wang, Bisimulation analysis of SDL-expressed protocols: a case study, Proceedings of the 2000 conference of the Centre for Advanced Studies on Collaborative research, p.2, November 13-16, 2000, Mississauga, Ontario, Canada
Matthew B. Dwyer , Corina S. Pasareanu, Filter-based model checking of partial systems, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.189-202, Nov. 1998
Michael Baldamus , Jochen Schröder-Babo, p2b: a translation utility for linking promela and symbolic model checking (tool paper), Proceedings of the 8th international SPIN workshop on Model checking of software, p.183-191, May 2001, Toronto, Ontario, Canada
Marsha Chechik, SC(R)3: towards usability of formal methods, Proceedings of the 1998 conference of the Centre for Advanced Studies on Collaborative research, p.8, November 30-December 03, 1998, Toronto, Ontario, Canada
Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
Georg Gottlob , Erich Grädel , Helmut Veith, Linear time datalog and branching time logic, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
Adnan Aziz , Serdar Taşiran , Robert K. Brayton, BDD variable ordering for interacting finite state machines, Proceedings of the 31st annual conference on Design automation, p.283-288, June 06-10, 1994, San Diego, California, United States
Gleb Naumovich , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, Applying static analysis to software architectures, ACM SIGSOFT Software Engineering Notes, v.22 n.6, p.77-93, Nov. 1997
Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States
Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States
Armin Biere , Wolfgang Kunz, SAT and ATPG: Boolean engines for formal hardware verification, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.782-785, November 10-14, 2002, San Jose, California
Stefan Edelkamp , Alberto Lluch Lafuente , Stefan Leue, Directed explicit model checking with HSF-SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.57-79, May 2001, Toronto, Ontario, Canada
Shiu-Kai Chin, High-confidence design for security: don't trust—verify, Communications of the ACM, v.42 n.7, p.33-37, July 1999
Farn Wang , Pao-Ann Hsiung, Efficient and User-Friendly Verification, IEEE Transactions on Computers, v.51 n.1, p.61-83, January 2002
P. Azzoni , A. Fedeli , F. Fummi , G. Pravadelli , U. Rossi , F. Toto, An error simulation based approach to measure error coverage of formal properties, Proceedings of the 12th ACM Great Lakes symposium on VLSI, April 18-19, 2002, New York, New York, USA
Hans Eveking, (V)HDL-based verification of heterogeneous synchronous/asynchronous systems, Proceedings of the conference on European design automation, p.566-571, September 19-23, 1994, Grenoble, France
Jean-Claude Fernandez , Marius Bozga , Lucian Ghirvu, State space reduction based on live variables analysis, Science of Computer Programming, v.47 n.2-3, p.203-220, May 2003
Harry Hsieh , Felice Balarin , Luciano Lavagno , Alberto Sangiovanni-Vincentelli, Efficient methods for embedded system design space exploration, Proceedings of the 37th conference on Design automation, p.607-612, June 05-09, 2000, Los Angeles, California, United States
Matthew Dwyer , John Hatcliff , Muhammad Nanda, Using partial evaluation to enable verification of concurrent software, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998
Yufeng Luo , Tjahjadi Wongsonegoro , Adnan Aziz, Hybrid techniques for fast functional simulation, Proceedings of the 35th annual conference on Design automation, p.664-667, June 15-19, 1998, San Francisco, California, United States
Patrice Godefroid , David E. Long, Symbolic Protocol Verification with Queue BDDs, Formal Methods in System Design, v.14 n.3, p.257-271, May 1999
Daniel Kroening , Wolfgang J. Paul, Automated pipeline design, Proceedings of the 38th conference on Design automation, p.810-815, June 2001, Las Vegas, Nevada, United States
Malay K. Ganai , Aarti Gupta , Pranav Ashar, Beyond safety: customized SAT-based model checking, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Karsten Strehl , Lothar Thiele, Symbolic model checking of process networks using interval diagram techniques, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.686-692, November 08-12, 1998, San Jose, California, United States
Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , Jim Kukula , Tom Shiple , Helmut Veith , Dong Wang, Non-linear quantification scheduling in image computation, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
Parosh Aziz Abdulla , S. Purushothaman Iyer , Aletta Nylén, SAT-Solving the Coverability Problem for Petri Nets, Formal Methods in System Design, v.24 n.1, p.25-43, January 2004
T. Pascalin Amagbegnon , Uri E. Barkai, Verifying the Implementation of an Error Control Code, Formal Methods in System Design, v.22 n.2, p.155-161, March 2003
Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design, v.18 n.2, p.141-163, March 1, 2001
Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
José Creissac Campos, A formal approach to the usability engineering, Proceedings of the Latin American conference on Human-computer interaction, August 17-20, 2003, Rio de Janeiro, Brazil
Christoph Meinel , Christian Stangier, Algorithms and heuristics in VLSI design, Experimental algorithmics: from algorithm design to robust and efficient software, Springer-Verlag New York, Inc., New York, NY, 2002
William N. Robinson , Suzanne D. Pawlowski , Vecheslav Volkov, Requirements interaction management, ACM Computing Surveys (CSUR), v.35 n.2, p.132-190, June 2003
Wolfgang Müller , Wolfgang Rosenstiel , Jürgen Ruf, References, SystemC: methodologies and applications, Kluwer Academic Publishers, Norwell, MA, 2003
Tatsuhiro Tsuchiya , Shin'ichi Nagano , Rohayu Bt Paidi , Tohru Kikuno, Symbolic Model Checking for Self-Stabilizing Algorithms, IEEE Transactions on Parallel and Distributed Systems, v.12 n.1, p.81-95, January 2001
Aarti Gupta , Malay Ganai , Chao Wang , Zijiang Yang , Pranav Ashar, Learning from BDDs in SAT-based bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Peter Revesz, A retrospective on constraint databases, Proceedings of the Paris C. Kanellakis memorial workshop on Principles of computing & knowledge: Paris C. Kanellakis memorial workshop on the occasion of his 50th birthday, p.12-27, June 08-08, 2003, San Diego, California, USA
Mauricio Varea , Bashir M. Al-Hashimi , Luis A. Cortés , Petru Eles , Zebo Peng, Symbolic model checking of Dual Transition Petri Nets, Proceedings of the tenth international symposium on Hardware/software codesign, May 06-08, 2002, Estes Park, Colorado
Hai Zhou, Clock schedule verification with crosstalk, Proceedings of the 8th ACM/IEEE international workshop on Timing issues in the specification and synthesis of digital systems, December 02-03, 2002, Monterey, California, USA
Tamir Heyman , Danny Geist , Orna Grumberg , Assaf Schuster, A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits, Formal Methods in System Design, v.21 n.3, p.317-338, November 2002
Mani Azimi , Ching-Tsun Chou , Akhilesh Kumar , Victor W. Lee , Phamndra K. Mannava , Seungjoon Park, Experience with Applying Formal Methods to Protocol Specification and System Architecture, Formal Methods in System Design, v.22 n.2, p.109-116, March 2003
Robert P. Kurshan , Vladimir Levin , Marius Minea , Doron Peled , Hüsnü Yenigün, Combining Software and Hardware Verification Techniques, Formal Methods in System Design, v.21 n.3, p.251-280, November 2002
Alessandro Fin , Franco Fummi , Graziano Pravadelli, Mixing ATPG and property checking for testing HW/SW interfaces, Proceedings of the 13th ACM Great Lakes symposium on VLSI, April 28-29, 2003, Washington, D. C., USA
Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
Gabriel Ciobanu , Dorel Lucanu, A specification language for coordinated objects, ACM SIGSOFT Software Engineering Notes, v.31 n.2, March 2006
Rune M. Jensen , Randal E. Bryant , Manuela M. Veloso, SetA*: an efficient BDD-based heuristic search algorithm, Eighteenth national conference on Artificial intelligence, p.668-673, July 28-August 01, 2002, Edmonton, Alberta, Canada
Marsha Chechik , Wei Ding, Lightweight reasoning about program correctness, Proceedings of the 2001 conference of the Centre for Advanced Studies on Collaborative research, p.1, November 05-07, 2001, Toronto, Ontario, Canada
A. Cimatti , M. Pistore , M. Roveri , P. Traverso, Weak, strong, and strong cyclic planning via symbolic model checking, Artificial Intelligence, v.147 n.1-2, p.35-84, July 2003
David A. Plaisted , Armin Biere , Yunshan Zhu, A satisfiability procedure for quantified boolean formulae, Discrete Applied Mathematics, v.130 n.2, p.291-328, 15 August 2003
Steven M. German, Formal Design of Cache Memory Protocols in IBM, Formal Methods in System Design, v.22 n.2, p.133-141, March 2003
Jonathan Whittle, Formal approaches to systems analysis using UML: an overview, Advanced topics in database research vol. 1, Idea Group Publishing, Hershey, PA, 2003
Tal Lev-Ami , Shmuel S. Tyszberowicz, Reactive and Real-Time Systems Course: How to Get the Most Out of it, Real-Time Systems, v.25 n.2-3, p.231-253, September-October 2003
Greg Dennis , Robert Seater , Derek Rayside , Daniel Jackson, Automating commutativity analysis at the design level, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Rajeev Alur , Radu Grosu, Modular refinement of hierarchic reactive machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.2, p.339-369, March 2004
V. Akella , G. Gopalakrishnan, Specification and Validation of Control-Intensive IC's in hopCP, IEEE Transactions on Software Engineering, v.20 n.6, p.405-423, June 1994
Françoise Casaubieilh , Anthony McIsaac , Mike Benjamin , Mike Bartley , François Pogodalla , Frédéric Rocheteau , Mohamed Belhadj , Jeremy Eggleton , Gérard Mas , Geoff Barrett , Christian Berthet, Functional verification methodology of Chameleon processor, Proceedings of the 33rd annual conference on Design automation, p.421-426, June 03-07, 1996, Las Vegas, Nevada, United States
Alberto L. Sangiovanni-Vincentelli , Patrick C. McGeer , Alexander Saldanha, Verification of electronic systems, Proceedings of the 33rd annual conference on Design automation, p.106-111, June 03-07, 1996, Las Vegas, Nevada, United States
Kirsten Winter, Model checking railway interlocking systems, Australian Computer Science Communications, v.24 n.1, p.303-310, January-February 2002
Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Henny B. Sipma , Tomás E. Uribe , Zohar Manna, Deductive Model Checking, Formal Methods in System Design, v.15 n.1, p.49-74, July 1999
Sofiène Tahar , Paul Curzon, Comparing HOL and MDG: a case study on the verification of an ATM switch fabric, Nordic Journal of Computing, v.6 n.4, p.372-402, Winter 1999
A. Aziz , F. Balarin , S.-T. Cheng , R. Hojati , T. Kam , S. C. Krishnan , R. K. Ranjan , T. R. Shiple , V. Singhal , S. Tasiran , H.-Y. Wang , R. K. Brayton , A. L. Sangiovanni-Vincentelli, HSIS: a BDD-based environment for formal verification, Proceedings of the 31st annual conference on Design automation, p.454-459, June 06-10, 1994, San Diego, California, United States
Tevfik Bultan , Richard Gerber , Christopher League, Verifying systems with integer constraints and Boolean predicates: a composite approach, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.113-123, March 1998
Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
Axel van Lamsweerde, Requirements engineering in the year 00: a research perspective, Proceedings of the 22nd international conference on Software engineering, p.5-19, June 04-11, 2000, Limerick, Ireland
Wolfgang Günther , Andreas Hett , Bernd Becker, Application of linearly transformed BDDs in sequential verification, Proceedings of the 2001 conference on Asia South Pacific design automation, p.91-96, January 2001, Yokohama, Japan
Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
Jie Xu , Alexander Romanovsky , Robert J. Stroud , Avelino F. Zorzo , Ercument Canver , Friedrich von Henke, Rigorous Development of an Embedded Fault-Tolerant System Based on Coordinated Atomic Actions, IEEE Transactions on Computers, v.51 n.2, p.164-179, February 2002
Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002
Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.26-38, Sept. 2000
Bijan Alizadeh, Word level functional coverage computation, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
Javier Esparza , Keijo Heljanko, Implementing LTL model checking with net unfoldings, Proceedings of the 8th international SPIN workshop on Model checking of software, p.37-56, May 2001, Toronto, Ontario, Canada
Amy P. Felty , Kedar S. Namjoshi, Feature specification and automated conflict detection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.1, p.3-27, January 2003
Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, ACM SIGOPS Operating Systems Review, v.36 n.SI, Winter 2002
Arindam Chakrabarti , Patrice Godefroid, Software partitioning for effective automated unit testing, Proceedings of the 6th ACM & IEEE International conference on Embedded software, October 22-25, 2006, Seoul, Korea
Ásgeir Th. Eiríksson, Integrating formal verification methods with a conventional project design flow, Proceedings of the 33rd annual conference on Design automation, p.666-671, June 03-07, 1996, Las Vegas, Nevada, United States
Jørgen Staunstrup , Henrik Reif Andersen , Henrik Hulgaard , Jørn Lind-Nielsen , Kim G. Larsen , Gerd Behrmann , Kåre Kristoffersen , Arne Skou , Henrik Leerberg , Niels Bo Theilgaard, Practical Verification of Embedded Software, Computer, v.33 n.5, p.68-75, May 2000
Nazanin Mansouri , Ranga Vemuri, Automated Correctness Condition Generation for Formal Verification ofSynthesized RTL Designs, Formal Methods in System Design, v.16 n.1, p.59-91, Jan 1,2000
David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
Matt Kaufmann , J. S. Moore, An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, IEEE Transactions on Software Engineering, v.23 n.4, p.203-213, April 1997
Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996
Xudong He , Huiqun Yu , Tianjun Shi , Junhua Ding , Yi Deng, Formally analyzing software architectural specifications using SAM, Journal of Systems and Software, v.71 n.1-2, p.11-29, April 2004
Junbeom Yoo , Taihyo Kim , Sungdeok Cha , Jang-Soo Lee , Han Seong Son, A formal software requirements specification method for digital nuclear plant protection systems, Journal of Systems and Software, v.74 n.1, p.73-83, January 2005
Monika Vetterling , Guido Wimmel , Alexander Wisspeintner, Secure systems development based on the common criteria: the PalME project, ACM SIGSOFT Software Engineering Notes, v.27 n.6, November 2002
Natasha Sharygina , James Browne , Fei Xie , Robert Kurshan , Vladimir Levin, Lessons Learned from Model Checking a NASA Robot Controller, Formal Methods in System Design, v.25 n.2-3, p.241-270, September-November 2004
Ying Tsai Chang , Kwang Ting Tim Cheng, Induction-based gate-level verification of multipliers, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
Marsha Chechik , Benet Devereux , Steve Easterbrook , Arie Gurfinkel, Multi-valued symbolic model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.4, p.371-408, October 2003
Agostino Dovier , Carla Piazza , Alberto Policriti, An efficient algorithm for computing bisimulation equivalence, Theoretical Computer Science, v.311 n.1-3, p.221-256, 23 January 2004
William N. N. Hung , Xiaoyu Song , Guowu Yang , Jin Yang , Marek Perkowski, Quantum logic synthesis by symbolic reachability analysis, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Jonathan Edwards , Daniel Jackson , Emina Torlak , Vincent Yeung, Faster constraint solving with subtypes, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Batsayan Das , Dipankar Sarkar , Santanu Chattopadhyay, Model checking on state transition diagram, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.412-417, January 27-30, 2004, Yokohama, Japan
Görschwin Fey , Rolf Drechsler, Improving simulation-based verification by means of formal methods, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.640-643, January 27-30, 2004, Yokohama, Japan
Rafael Ramirez , Juanjo Martinez, Brief Announcement: constraint-based synchronization and verification of concurrent programs, Proceedings of the twenty-third annual ACM symposium on Principles of distributed computing, July 25-28, 2004, St. John's, Newfoundland, Canada
Orna Kupferman , Moshe Y. Vardi, From linear time to branching time, ACM Transactions on Computational Logic (TOCL), v.6 n.2, p.273-294, April 2005
Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001
Tuba Yavuz-Kahveci , Tevfik Bultan, Specification, verification, and synthesis of concurrency control components, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
Frédéric Herbreteau , Franck Cassez , Olivier Roux, Application of Partial-Order Methods to Reactive Programswith Event Memorization, Real-Time Systems, v.20 n.3, p.287-316, May 2001
Harald Rueß , Leonardo de Moura, Simulation and verification I: from simulation to verification (and back), Proceedings of the 35th conference on Winter simulation: driving innovation, December 07-10, 2003, New Orleans, Louisiana
Harald Rueß , Leonardo de Moura, Simulation and verification I: from simulation to verification (and back), Proceedings of the 35th conference on Winter simulation: driving innovation, December 07-10, 2003, New Orleans, Louisiana
Ganesh Gopalakrishnan, Developing Micropipeline Wavefront Arbiters, IEEE Design & Test, v.11 n.4, p.55-64, October 1994
John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000
Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004
William Chan , Richard J. Anderson , Paul Beame , David Notkin , David H. Jones , William E. Warner, Optimizing Symbolic Model Checking for Statecharts, IEEE Transactions on Software Engineering, v.27 n.2, p.170-190, February 2001
Jørn Lind-Nielsen , Henrik Reif Andersen , Henrik Hulgaard , Gerd Behrmann , Kåre Kristoffersen , Kim G. Larsen, Verification of Large State/Event Systems Using Compositionality and Dependency Analysis, Formal Methods in System Design, v.18 n.1, p.5-23, January.2001
Pamela Zave , Michael Jackson, Where Do Operations Come From? A Multiparadigm Specification Technique, IEEE Transactions on Software Engineering, v.22 n.7, p.508-528, July 1996
Hazem I. Shehata , Mark D. Aagaard, A general decomposition strategy for verifying register renaming, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Exploiting state encoding for invariant generation in induction-based property checking, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.424-429, January 27-30, 2004, Yokohama, Japan
Shuo Sheng , Michael S. Hsiao, Success-Driven Learning in ATPG for Preimage Computation, IEEE Design & Test, v.21 n.6, p.504-512, November 2004
William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998
A. Cimatti , M. Roveri , P. Bertoli, Conformant planning via symbolic model checking and heuristic search, Artificial Intelligence, v.159 n.1-2, p.127-206, November 2004
P. Baldan , N. Busi , A. Corradini , G. M. Pinna, Domain and event structure semantics for Petri nets with read and inhibitor arcs, Theoretical Computer Science, v.323 n.1-3, p.129-189, 14 September 2004
Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997
Axel van Lamsweerde , Laurent Willemet, Inferring Declarative Requirements Specifications from Operational Scenarios, IEEE Transactions on Software Engineering, v.24 n.12, p.1089-1114, December 1998
Thomas A. Henzinger , Orna Kupferman , Shaz Qadeer, From Pre-Historic to Post-Modern Symbolic Model Checking, Formal Methods in System Design, v.23 n.3, p.303-327, November 2003
Axel van Lamsweerde , Emmanuel Letier, Handling Obstacles in Goal-Oriented Requirements Engineering, IEEE Transactions on Software Engineering, v.26 n.10, p.978-1005, October 2000
Bishop C. Brock , Warren A. Hunt, Jr., The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor, Formal Methods in System Design, v.11 n.1, p.71-104, July 1997
Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995
Axel van Lamsweerde , Emmanual Letier , Robert Darimont, Managing Conflicts in Goal-Driven Requirements Engineering, IEEE Transactions on Software Engineering, v.24 n.11, p.908-926, November 1998
Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
Raffaella Gentilini , Carla Piazza , Alberto Policriti, Computing strongly connected components in a linear number of symbolic steps, Proceedings of the fourteenth annual ACM-SIAM symposium on Discrete algorithms, January 12-14, 2003, Baltimore, Maryland
Design and Analysis of a Self-Timed Duplex Communication System, IEEE Transactions on Computers, v.53 n.7, p.798-814, July 2004
James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996
Stephen F. Seigel , George S. Avrunin, Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles, IEEE Transactions on Software Engineering, v.28 n.2, p.115-128, February 2002
Jochen Klose , Thomas Kropf , Jürgen Ruf, A visual approach to validating system level designs, Proceedings of the 15th international symposium on System Synthesis, October 02-04, 2002, Kyoto, Japan
Gaoyan Xie , Cheng Li , Zhe Dang, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Theoretical Computer Science, v.328 n.1-2, p.203-219, 29 November 2004
Ian G. Harris, Fault Models and Test Generation for Hardware-Software Covalidation, IEEE Design & Test, v.20 n.04, p.40-47, January 2003
Alex Semenov , Albert M. Koelmans , Lee Lloyd , Alexandre Yakovlev, Designing an Asynchronous Processor Using Petri Nets, IEEE Micro, v.17 n.2, p.54-64, March 1997
Jia Xu, On Inspection and Verification of Software with Timing Requirements, IEEE Transactions on Software Engineering, v.29 n.8, p.705-720, August 2003
Cormac Flanagan, Automatic software model checking via constraint logic, Science of Computer Programming, v.50 n.1-3, p.253-270, March 2004
Hana Chockler , Orna Kupferman, ω-Regular languages are testable with a constant number of queries, Theoretical Computer Science, v.329 n.1-3, p.71-92, 13 December 2004
Noppanunt Utamaphethai , R. D. Shawn Blanton , John Paul Shen, Effectiveness of Microarchitecture Test Program Generation, IEEE Design & Test, v.17 n.4, p.38-49, October 2000
Antonella Santone , Gigliola Vaglini, A local approach for temporal model checking of java bytecode, Journal of Computer and System Sciences, v.70 n.2, p.258-281, March 2005
Weibo Mao , Jinzhao Wu, Application of Wu's method to symbolic model checking, Proceedings of the 2005 international symposium on Symbolic and algebraic computation, p.237-244, July 24-27, 2005, Beijing, China
Freddy Y.C. Mang , Pei-Hsin Ho, Abstraction refinement by controllability and cooperativeness analysis, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Alexander Holt , Ewan Klein, A semantically-derived subset of English for hardware verification, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.451-456, June 20-26, 1999, College Park, Maryland
Debashis Sahoo , Jawahar Jain , Subramanian K. Iyer , David L. Dill , E. Allen Emerson, Multi-threaded reachability, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Rik Eshuis, Symbolic model checking of UML activity diagrams, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.1, p.1-38, January 2006
David Stotts , Jaime Navon, Model checking cobweb protocols for verification of HTML frames behavior, Proceedings of the 11th international conference on World Wide Web, May 07-11, 2002, Honolulu, Hawaii, USA
Syed M. Suhaib , Deepak A. Mathaikutty , Sandeep K. Shukla , David Berner, XFM: An incremental methodology for developing formal models, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.4, p.589-609, October 2005
Xi Chen , Abhijit Davare , Harry Hsieh , Alberto Sangiovanni-Vincentelli , Yosinori Watanabe, Simulation based deadlock analysis for system level designs, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Natarajan Shankar, Automated verification using deduction, exploration, and abstraction, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
K. Rustan M. Leino , Todd Millstein , James B. Saxe, Generating error traces from verification-condition counterexamples, Science of Computer Programming, v.55 n.1-3, p.209-226, March 2005
Lubomir Ivanov, Integrating formal verification into computer organization and architecture courses, Journal of Computing Sciences in Colleges, v.17 n.3, p.115-124, February 2002
R. F. Lutje Spelberg , W. J. Toetenel, Parametric real-time model checking using splitting trees, Nordic Journal of Computing, v.8 n.1, p.88-120, Spring 2001
S. Chouali , J. Julliand , P.-A. Masson , F. Bellegarde, PLTL-partitioned model checking for reactive systems under fairness assumptions, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.267-301, May 2005
Thomas Eiter , Michael Fink , Giuliana Sabbatini , Hans Tompits, Reasoning about evolving nonmonotonic knowledge bases, ACM Transactions on Computational Logic (TOCL), v.6 n.2, p.389-440, April 2005
Rajeev Alur , Swarat Chaudhuri , P. Madhusudan, A fixpoint calculus for local and global program flows, ACM SIGPLAN Notices, v.41 n.1, p.153-165, January 2006
Sara Gradara , Antonella Santone , Maria Luisa Villani, Using heuristic search for finding deadlocks in concurrent systems, Information and Computation, v.202 n.2, p.191-226, 1 November, 2005
Yirng-An Chen , Fang-Sung Chen, Algorithms for compacting error traces, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
R. E. K. Stirewalt , Min Deng , Betty H. C. Cheng, UML formalization is a traceability problem, Proceedings of the 3rd international workshop on Traceability in emerging forms of software engineering, November 08-08, 2005, Long Beach, California
Olivier Tardieu , Robert de Simone, Loops in esterel, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.4, p.708-750, November 2005
Hyoung Seok Hong , Sung Deok Cha , Insup Lee , Oleg Sokolsky , Hasan Ural, Data flow testing as model checking, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Julia Dushina , Mike Benjamin , Daniel Geist, Semi-formal test generation and resolving a temporal abstraction problem in practice: industrial application, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
Monika Vetterling , Guido Wimmel , Alexander Wisspeintner, Secure systems development based on the common criteria: the PalME project, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA
Marcelo F. Frias , Carlos G. López Pombo , Gabriel A. Baum , Nazareno M. Aguirre , Thomas S. E. Maibaum, Reasoning about static and dynamic properties in alloy: A purely relational approach, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.4, p.478-526, October 2005
R. H. Hardin , R. P. Kurshan , S. K. Shukla , M. Y. Vardi, A New Heuristic for Bad Cycle Detection Using BDDs, Formal Methods in System Design, v.18 n.2, p.131-140, March 1, 2001
Satoshi Yamane, Automatic effective verification method for distributed and concurrent systems using timed language inclusion, Engineering of distributed control systems, Nova Science Publishers, Inc., Commack, NY, 2001
Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

, December 09-11, 2002, Boston, Massachusetts
Ralph D. Jeffords , Constance L. Heitmeyer, A strategy for efficiently verifying requirements, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, v.10 n.1, p.47-71, February 1997
Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003
Michael Shute, SPPV: a new formal verification environment, Journal of Computing Sciences in Colleges, v.17 n.6, p.292-294, May 2002
Martin Deubler , Johannes Grünbauer , Jan Jürjens , Guido Wimmel, Sound development of secure service-based systems, Proceedings of the 2nd international conference on Service oriented computing, November 15-19, 2004, New York, NY, USA
Sérgio Campos , Berthier Ribeiro-Neto , Autran Macedo , Luciano Bertini, Formal verification and analysis of multimedia systems, Proceedings of the seventh ACM international conference on Multimedia (Part 1), p.419-430, October 30-November 05, 1999, Orlando, Florida, United States
Jianbin Tan , George S. Avrunin , Lori A. Clarke, Managing space for finite-state verification, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
Antonella Santone , Gigliola Vaglini, Local model checking of Java bytecode, Proceedings of the 14th international conference on Software engineering and knowledge engineering, July 15-19, 2002, Ischia, Italy
R. M. Gott , J. R. Baumgartner , P. Roessler , S. I. Joe, Functional formal verification on designs of pSeries microprocessors and communication subsystems, IBM Journal of Research and Development, v.49 n.4/5, p.565-580, July 2005
Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
Hue-Min Lin , Chia-Chih Yen , Che-Hua Shih , Jing-Yang Jou, On compliance test of on-chip bus for SOC, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.328-333, January 27-30, 2004, Yokohama, Japan
Thomas A. Henzinger , Orna Kupferman , Rupak Majumdar, On the universal and existential fragments of the μ-calculus, Theoretical Computer Science, v.354 n.2, p.173-186, 28 March 2006
Michael S. Hsiao , Shuo Sheng , Rajat Arora , Ankur Jain , Vamsi Boppana, Verification of large scale nano systems with unreliable nano devices, Nano, quantum and molecular computing: implications to high level design and validation, Kluwer Academic Publishers, Norwell, MA, 2004
Ziv Nevo , Monica Farkash, Distributed dynamic BDD reordering, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Strong planning under partial observability, Artificial Intelligence, v.170 n.4, p.337-384, April 2006
Chao Wang , Roderick Bloem , Gary D. Hachtel , Kavita Ravi , Fabio Somenzi, Compositional SCC Analysis for Language Emptiness, Formal Methods in System Design, v.28 n.1, p.5-36, January 2006
Roderick Bloem , Harold N. Gabow , Fabio Somenzi, An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps, Formal Methods in System Design, v.28 n.1, p.37-56, January 2006
Iñigo Ugarte , Pablo Sanchez, Verification of embedded systems based on interval analysis, International Journal of Parallel Programming, v.33 n.6, p.697-720, December 2005
Felix Sheng-Ho Chang , Daniel Jackson, Symbolic model checking of declarative relational models, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
Christoph Meinel , Christian Stangier, Data structures for Boolean functions, Computational Discrete Mathematics: advanced lectures, Springer-Verlag New York, Inc., New York, NY, 2001
Rance Cleaveland , S. Purushothaman Iyer , Murali Narasimha, Probabilistic temporal logics via the modal mu-calculus, Theoretical Computer Science, v.342 n.2-3, p.316-350, 7 September 2005
Nicola Bombieri , Franco Fummi , Graziano Pravadelli, On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
Constance Heitmeyer, Developing safety-critical systems: the role of formal methods and tools, Proceedings of the 10th Australian workshop on Safety critical systems and software, p.95-99, August 25, 2005, Sydney, Australia
K. Winter , W. Johnston , P. Robinson , P. Strooper , L. van den Berg, Tool support for checking railway interlocking designs, Proceedings of the 10th Australian workshop on Safety critical systems and software, p.101-107, August 25, 2005, Sydney, Australia
Jamieson M. Cobleigh , George S. Avrunin , Lori A. Clarke, Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-52, April 2008
Franco Fummi , Graziano Pravadelli, Too Few or Too Many Properties? Measure it by ATPG!, Journal of Electronic Testing: Theory and Applications, v.23 n.5, p.373-388, October 2007
Bart Jacobs, The temporal logic of coalgebras via Galois algebras, Mathematical Structures in Computer Science, v.12 n.6, p.875-903, December 2002
Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for embedded software verification, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
Vishnu C. Vimjam , Michael S. Hsiao, Fast illegal state identification for improving SAT-based induction, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Pieter H. Hartel , Luc Moreau, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Computing Surveys (CSUR), v.33 n.4, p.517-558, December 2001
Matthew B. Dwyer , Vicki Carr , Laura Hines, Model checking graphical user interfaces using abstractions, ACM SIGSOFT Software Engineering Notes, v.22 n.6, p.244-261, Nov. 1997
Rachel L. Cobleigh , George S. Avrunin , Lori A. Clarke, User guidance for creating precise and accessible property specifications, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
Orna Grumberg , Tamir Heyman , Assaf Schuster, A work-efficient distributed algorithm for reachability analysis, Formal Methods in System Design, v.29 n.2, p.157-175, September 2006
Wan Fokkink , Jaap-Henk Hoepman , Jun Pang, A note on K-state self-stabilization in a ring with K = N, Nordic Journal of Computing, v.12 n.1, p.18-26, March 2005
Ben Denckla, Many cyclic block diagrams do not need parallel semantics, ACM SIGPLAN Notices, v.41 n.8, August 2006
Sara Gradara , Antonella Santone , Maria Luisa Villani, DELFIN+: An efficient deadlock detection tool for CCS processes, Journal of Computer and System Sciences, v.72 n.8, p.1397-1412, December, 2006
James Cheney , Alberto Momigliano, Mechanized metatheory model-checking, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
Luca P. Carloni , Roberto Passerone , Alessandro Pinto , Alberto L. Angiovanni-Vincentelli, Languages and tools for hybrid systems design, Foundations and Trends® in Electronic Design Automation, v.1 n.1/2, p.1-193, June 2006
Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
Claudio de la Riva , Javier Tuya, Automatic generation of assumptions for modular verification of software specifications, Journal of Systems and Software, v.79 n.9, p.1324-1340, September 2006
Muffy Calder , Alice Miller, Feature interaction detection by pairwise analysis of LTL properties: a case study, Formal Methods in System Design, v.28 n.3, p.213-261, May 2006
Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, ACM SIGPLAN Notices, v.41 n.10, October 2006
Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
Hong Liu , David P. Gluch, Templates and automation for temporal query generation, Proceedings of the 44th annual southeast regional conference, March 10-12, 2006, Melbourne, Florida
George S. Avrunin , Stephen F. Siegel , Andrew R. Siegel, Finite-state verification for high performance computing, Proceedings of the second international workshop on Software engineering for high performance computing system applications, May 15-15, 2005, St. Louis, Missouri
Mauricio Varea , Bashir M. Al-Hashimi , Luis A. CortéS , Petru Eles , Zebo Peng, Dual Flow Nets: Modeling the control/data-flow relation in embedded systems, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.1, p.54-81, February 2006
Mohammad Mahdi Jaghoori , Ali Movaghar , Marjan Sirjani, Modere: the model-checking engine of Rebeca, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
Ali Habibi , Haja Moinudeen , Sofiène Tahar, Generating finite state machines from SystemC, Proceedings of the conference on Design, automation and test in Europe: Designers' forum, March 06-10, 2006, Munich, Germany
Minmin Han , Christine Hofmeister, Modeling and verification of adaptive navigation in web applications, Proceedings of the 6th international conference on Web engineering, July 11-14, 2006, Palo Alto, California, USA
Greg Dennis , Felix Sheng-Ho Chang , Daniel Jackson, Modular verification of code with SAT, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Marsha Chechik , Arie Gurfinkel , Benet Devereux , Albert Lai , Steve Easterbrook, Data structures for symbolic multi-valued model-checking, Formal Methods in System Design, v.29 n.3, p.295-344, November 2006
Wu-Hon F. Leung, Program entanglement, feature interaction and the feature language extensions, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.51 n.2, p.480-495, February, 2007
Yves Bontemps , Patrick Heymans , Pierre-Yves Schobbens, From Live Sequence Charts to State Machines and Back: A Guided Tour, IEEE Transactions on Software Engineering, v.31 n.12, p.999-1014, December 2005
W. L. Yeung , K. R. P. H. Leung , Ji Wang , Wei Dong, Modelling and model checking suspendible business processes via statechart diagrams and CSP, Science of Computer Programming, v.65 n.1, p.14-29, March, 2007
Shireesh Verma , Ian G. Harris , Kiran Ramineni, Interactive presentation: Automatic generation of functional coverage models from behavioral verilog descriptions, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Rina Dechter , Robert Mateescu, AND/OR search spaces for graphical models, Artificial Intelligence, v.171 n.2-3, p.73-106, February, 2007
Miquel Bertran , Francesc Babot , August Climent, Formal Sequentialization of Distributed Systems via Program Rewriting, Electronic Notes in Theoretical Computer Science (ENTCS), 188, p.53-75, July, 2007
Henry Kautz , Bart Selman, The state of SAT, Discrete Applied Mathematics, v.155 n.12, p.1514-1524, June, 2007
Sara Gradara , Antonella Santone , Maria Luisa Villani, Formal Verification of Concurrent Systems via Directed Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), 185, p.93-105, July, 2007
Kazuhiro Ogata , Kokichi Futatsugi, Modeling and verification of real-time systems based on equations, Science of Computer Programming, v.66 n.2, p.162-180, April, 2007
Manfred Droste , Paul Gastin, Weighted automata and weighted logics, Theoretical Computer Science, v.380 n.1-2, p.69-86, June, 2007
Wiebe van der Hoek , Alessio Lomuscio , Michael Wooldridge, On the complexity of practical ATL model checking, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, May 08-12, 2006, Hakodate, Japan
Alma L. Juarez-Dominguez , Nancy A. Day , Jeffrey J. Joyce, Modelling feature interactions in the automotive domain, Proceedings of the 2008 international workshop on Models in software engineering, May 10-11, 2008, Leipzig, Germany
Conghua Zhou, A compositional symbolic verification framework for concurrent software, Proceedings of the 2nd international conference on Scalable information systems, June 06-08, 2007, Suzhou, China
Peter Buneman , Martin Grohe , Christoph Koch, Path queries on compressed XML, Proceedings of the 29th international conference on Very large data bases, p.141-152, September 09-12, 2003, Berlin, Germany
Quocnam Tran , Moshe Y. Vardi, Groebner bases computation in Boolean rings for symbolic model checking, Proceedings of the 18th conference on Proceedings of the 18th IASTED International Conference: modelling and simulation, p.440-445, May 30-June 01, 2007, Montreal, Canada
Paolo Baldan , Andrea Corradini , Barbara König, A framework for the verification of infinite-state graph transformation systems, Information and Computation, v.206 n.7, p.869-907, July, 2008
David Ward , Fabio Somenzi, Decomposing image computation for symbolic reachability analysis using control flow information, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for software verification, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.12 n.2, p.10-es, April 2007
Sanjit A. Seshia , Wenchao Li , Subhasish Mitra, Verification-guided soft error resilience, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Chikatoshi Yamada , Yasunori Nagata, An efficient specification for model checking using check-points extraction method, Proceedings of the 7th Conference on 7th WSEAS International Conference on Applied Computer Science, p.208-213, November 21-23, 2007, Venice, Italy
Sascha Klüppelholz , Christel Baier, Symbolic Model Checking for Channel-based Component Connectors, Electronic Notes in Theoretical Computer Science (ENTCS), v.175 n.2, p.19-37, June, 2007
Adilson Luiz Bonifácio , Arnaldo Vieira Moura , Adenilso da Silva Simão , José Carlos Maldonado, Towards Deriving Test Sequences by Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), 195, p.21-40, January, 2008
Sarfraz Khurshid , Darko Marinov, TestEra: Specification-Based Testing of Java Programs Using SAT, Automated Software Engineering, v.11 n.4, p.403-434, October 2004
Liang Zhang , M. R. Prasad , M. S. Hsiao, Incremental deductive & inductive reasoning for SAT-based bounded model checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.502-509, November 07-11, 2004
M. K. Ganai , A. Gupta , P. Ashar, Efficient SAT-based unbounded symbolic model checking using circuit cofactoring, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.510-517, November 07-11, 2004
Bing Li , F. Somenzi, Efficient computation of small abstraction refinements, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.518-525, November 07-11, 2004
A. Kuehlmann, Dynamic transition relation simplification for bounded property checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.50-57, November 07-11, 2004
Marek A. Bednarczyk , Wojciech Jamroga , Wiesław Pawłowski, Expressing and Verifying Temporal and Structural Properties of Mobile Agents, Fundamenta Informaticae, v.72 n.1-3, p.51-63, January 2006
Alessio Lomuscio , Wojciech Penczek, Symbolic model checking for temporal-epistemic logics, ACM SIGACT News, v.38 n.3, September 2007
Shinichi Honiden , Yasuyuki Tahara , Nobukazu Yoshioka , Kenji Taguchi , Hironori Washizaki, Top SE: Educating Superarchitects Who Can Apply Software Engineering Tools to Practical Development in Japan, Proceedings of the 29th International Conference on Software Engineering, p.708-718, May 20-26, 2007
Walter Dosch , Pornsiri Muenchaisri , Wuttipong Ruanthong , Annette Stümpel, Model checking for input/output properties of a black-box model, Proceedings of the third conference on IASTED International Conference: Advances in Computer Science and Technology, p.120-127, April 02-04, 2007, Phuket, Thailand
Mana Taghdiri , Daniel Jackson, Inferring specifications to detect errors in code, Automated Software Engineering, v.14 n.1, p.87-121, March 2007
Moreno Falaschi , Alicia Villanueva, Automatic verification of timed concurrent constraint programs, Theory and Practice of Logic Programming, v.6 n.3, p.265-300, May 2006
E. Dubrova , M. Teslenko , A. Martinelli, Kauffman networks: analysis and applications, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.479-484, November 06-10, 2005, San Jose, CA
Oleg Sokolsky , Insup Lee , Hanêne Ben-Abdallah, Specification and analysis of real-time systems with PARAGON, Annals of Software Engineering, v.7 n.1-4, p.211-234, 1999
Dimitra Giannakopoulou , Corina S. Pasareanu , Jamieson M. Cobleigh, Assume-Guarantee Verification of Source Code with Design-Level Assumptions, Proceedings of the 26th International Conference on Software Engineering, p.211-220, May 23-28, 2004
R. P. Kurshan , M. Merritt , A. Orda , S. R. Sachs, Modelling Asynchrony with a Synchronous Model, Formal Methods in System Design, v.15 n.3, p.175-199, Nov. 1999
Noppanunt Utamaphethai , R. D. (Shawn) Blanton , John Paul Shen, A Buffer-Oriented Methodology for Microarchitecture Validation, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.49-65, Feb/April 2000
Tevfik Bultan, A composite model checking toolset for analyzing software systems, ACM SIGSOFT Software Engineering Notes, v.25 n.1, p.37-38, Jan 2000
Matthew B. Dwyer , John Hatcliff, Adapting programming languages technologies for finite-state verification, ACM SIGSOFT Software Engineering Notes, v.25 n.1, p.46-49, Jan 2000
Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Automatic Vector Generation Using Constraints and Biasing, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.107-120, Feb/April 2000
Jianbin Tan , George S. Avrunin , Lori A. Clarke, Heuristic-Based Model Refinement for FLAVERS, Proceedings of the 26th International Conference on Software Engineering, p.635-644, May 23-28, 2004
Dimitra Giannakopoulou , Jeff Kramer , Shing Chi Cheung, Behaviour Analysis of Distributed Systems Using the Tracta Approach, Automated Software Engineering, v.6 n.1, p.7-35, January 1999
Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999
José C. Campos , Michael D. Harrison, Model Checking Interactor Specifications, Automated Software Engineering, v.8 n.3-4, p.275-310, August 2001
David A. Schmidt, Trace-Based Abstract Interpretation of Operational Semantics, Lisp and Symbolic Computation, v.10 n.3, p.237-271, May 1998
M. Huhn , K. Schneider , Th. Kropf , G. Logothetis, Verifying imprecisely working arithmetic circuits, Proceedings of the conference on Design, automation and test in Europe, p.13-es, January 1999, Munich, Germany
Farn Wang , Chia-Tien Lo, Procedure-Level Verification of Real-time Concurrent Systems, Real-Time Systems, v.16 n.1, p.81-114, Jan. 1999
Malay Ganai , Praveen Yalagandula , Adnan Aziz , Andreas Kuehlmann , Vigyan Singhal, SIVA: A System for Coverage-Directed State Space Search, Journal of Electronic Testing: Theory and Applications, v.17 n.1, p.11-27, February 2001
Nikolaj S. Bjørner , Anca Browne , Michael A. Colón , Bernd Finkbeiner , Zohar Manna , Henny B. Sipma , Tomás E. Uribe, Verifying Temporal Properties of Reactive Systems: A STeP Tutorial, Formal Methods in System Design, v.16 n.3, p.227-270, June 2000
Mark Hoogendoorn , Jan Treur, An Adaptive Multi-agent Organization Model Based on Dynamic Role Allocation, Proceedings of the IEEE/WIC/ACM international conference on Intelligent Agent Technology, p.474-481, December 18-22, 2006
M. Kacprzak , A. Lomuscio , W. Penczek, From Bounded to Unbounded Model Checking for Temporal Epistemic Logic, Fundamenta Informaticae, v.63 n.2-3, p.221-240, April 2004
Markus Stumptner , Franz Wotawa, A survey of intelligent debugging, AI Communications, v.11 n.1, p.35-51, January 1998
Bożena Woźna, ACTLS properties and Bounded Model Checking, Fundamenta Informaticae, v.63 n.1, p.65-87, January 2004
A. N. Chebotarev, The Automata-Theoretic Approach to Verification of Reactive Systems, Cybernetics and Systems Analysis, v.37 n.6, p.810-819, November-December 2001
Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar, Iterative Abstraction using SAT-based BMC with Proof Analysis, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.416, November 09-13, 2003
Chikatoshi Yamada , Yasunori Nagata, A check-points extraction method for formal verification, Proceedings of the 7th Conference on 7th WSEAS International Conference on Systems Theory and Scientific Computation, p.78-83, August 24-26, 2007, Vouliagmeni, Athens, Greece
Peter Muth , Dirk Wodtke , Jeanine Weissenfels , Angelika Kotz Dittrich , Gerhard Weikum, From Centralized Workflow Specification to Distributed WorkflowExecution, Journal of Intelligent Information Systems, v.10 n.2, p.159-184, March/April 1998
Hai Zhou, Timing Verification with Crosstalk for Transparently Latched Circuits, Proceedings of the conference on Design, Automation and Test in Europe, p.10056, March 03-07, 2003
Axel Poigné , Matthew Morley , Olivier Maffeïs , Leszek Holenderski , Reinhard Budde, The Synchronous Approach to Designing Reactive Systems, Formal Methods in System Design, v.12 n.2, p.163-187, March 1, 1998
J. Froessl , Th. Kropf , J. Gerlach, An Efficient Algorithm for Real-Time Symbolic Model Checking, Proceedings of the 1996 European conference on Design and Test, p.15, March 11-14, 1996
S. L. Kryvyi , L. Ye. Matveyeva, Formal Methods of Analysis of System Properties, Cybernetics and Systems Analysis, v.39 n.2, p.174-191, March-April 2003
Mark Reith , Jianwei Niu , William H. Winsborough, Role-based trust management security policy analysis and correction environment (RT-SPACE), Companion of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
Malay K. Ganai , Aarti Gupta , Pranav Ashar, Verification of Embedded Memory Systems using Efficient Memory Modeling, Proceedings of the conference on Design, Automation and Test in Europe, p.1096-1101, March 07-11, 2005
M. Borgatti , A. Capello , U. Rossi , J.-L. Lambert , I. Moussa , F. Fummi , G. Pravadelli, An Integrated Design and Verification Methodology for Reconfigurable Multimedia Systems, Proceedings of the conference on Design, Automation and Test in Europe, p.266-271, March 07-11, 2005
Ali Habibi , Asif Iqbal Ahmed , Otmane Ait Mohamed , Sofiene Tahar, On the Design and Verification Methodology of the Look-Aside Interface, Proceedings of the conference on Design, Automation and Test in Europe, p.290-295, March 07-11, 2005
Wolfgang Kuuml;chlin , Carsten Sinz, Proving Consistency Assertions for Automotive Product Data Management, Journal of Automated Reasoning, v.24 n.1-2, p.145-163, February 2000
Jessica Chen, On Verifying Distributed Multithreaded Java Programs, Software Quality Control, v.8 n.4, p.321-341, December 1999
Marsha Chechik , Wei Ding, Lightweight Reasoning about Program Correctness, Information Systems Frontiers, v.4 n.4, p.363-377, December 2002
Peter Buchholz , Peter Kemper, Efficient Computation and Representation of Large Reachability Sets for Composed Automata, Discrete Event Dynamic Systems, v.12 n.3, p.265-286, July 2002
Christoph Kreitz, Building reliable, high-performance networks with the Nuprl proof development system, Journal of Functional Programming, v.14 n.1, p.21-68, January 2004
Marc-Michel Corsini , Antoine Rauzy, Toupie: The µ-calculus over Finite Domains as a Constraint Language, Journal of Automated Reasoning, v.19 n.2, p.143-171, October 1997
R. Gentilini , C. Piazza , A. Policriti, From Bisimulation to Simulation: Coarsest Partition Problems, Journal of Automated Reasoning, v.31 n.1, p.73-103, 2003
Rune M. Jensen , Manuela M. Veloso , Randal E. Bryant, State-set branching: Leveraging BDDs for heuristic search, Artificial Intelligence, v.172 n.2-3, p.103-139, February, 2008
Jochen Eisinger , Felix Klaedtke, Don't care words with an application to the automata-based approach for real addition, Formal Methods in System Design, v.33 n.1-3, p.85-115, December 2008
Nicola Bombieri , Franco Fummi , Graziano Pravadelli, Reuse and optimization of testbenches and properties in a TLM-to-RTL design flow, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.3, p.1-22, July 2008
Malay Ganai , Aarti Gupta, Tunneling and slicing: towards scalable BMC, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California
M. Calder , A. Miller, An automatic abstraction technique for verifying featured, parameterised systems, Theoretical Computer Science, v.404 n.3, p.235-255, September, 2008
Julian Dolby , Mandana Vaziri , Frank Tip, Finding bugs efficiently with a SAT solver, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
A. Gawanmeh , S. Tahar , K. Winter, Formal verification of ASMs using MDGs, Journal of Systems Architecture: the EUROMICRO Journal, v.54 n.1-2, p.15-34, January, 2008
Younes Lahbib , Meriam Kallel , Ayoub Dhouib , Maher Hechkel , Antoine Perrin , Rached Tourki, System on Chips optimization using ABV and automatic generation of SystemC codes, Microprocessors & Microsystems, v.31 n.7, p.433-444, November, 2007
Lee Pike, Model checking for the practical verificationist: a user's perspective on SAL, Proceedings of the second workshop on Automated formal methods, p.21-31, November 06-06, 2007, Atlanta, Georgia
Tobias Nopper , Christoph Scholl , Bernd Becker, Computation of minimal counterexamples by using black box techniques and symbolic methods, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Matteo Pradella , Angelo Morzenti , Pierluigi San Pietro, The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
Sophie Laplante , Richard Lassaigne , Frédéric Magniez , Sylvain Peyronnet , Michel de Rougemont, Probabilistic abstraction for model checking: An approach based on property testing, ACM Transactions on Computational Logic (TOCL), v.8 n.4, p.20-es, August 2007
Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, Formal methods for the analysis and synthesis of nanometer-scale cellular arrays, ACM Journal on Emerging Technologies in Computing Systems (JETC), v.4 n.2, p.1-27, April 2008
Wojciech Jamroga , Thomas Ågotnes, Modular interpreted systems, Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, May 14-18, 2007, Honolulu, Hawaii
Michael Schäfer , Peter Dolog , Wolfgang Nejdl, An environment for flexible advanced compensations of Web service transactions, ACM Transactions on the Web (TWEB), v.2 n.2, p.1-36, April 2008
Bożena Woźna , Andrzej Zbrzezny, Bounded Model Checking for the Existential Fragment of TCTL_{-G} and Diagonal Timed Automata, Fundamenta Informaticae, v.79 n.1-2, p.229-256, January 2007
Agata Janowska , Wojciech Penczek, Path Compression in Timed Automata, Fundamenta Informaticae, v.79 n.3-4, p.379-399, August 2007
Mirosław Kurkowski , Wojciech Penczek, Verifying Security Protocols Modelled by Networks of Automata, Fundamenta Informaticae, v.79 n.3-4, p.453-471, August 2007
Franjo Ivani , Zijiang Yang , Malay K. Ganai , Aarti Gupta , Pranav Ashar, Efficient SAT-based bounded model checking for software verification, Theoretical Computer Science, v.404 n.3, p.256-274, September, 2008
Calvin Kai Fan Tang , Eugenia Ternovska, Model Checking Abstract State Machines with Answer Set Programming, Fundamenta Informaticae, v.77 n.1-2, p.105-141, January 2007
Anubhav Gupta , K. L. Mcmillan , Zhaohui Fu, Automated assumption generation for compositional verification, Formal Methods in System Design, v.32 n.3, p.285-301, June 2008
Tertia Hörne , John A. van der Poll, Planning as model checking: the performance of ProB vs NuSMV, Proceedings of the 2008 annual research conference of the South African Institute of Computer Scientists and Information Technologists on IT research in developing countries: riding the wave of technology, p.114-123, October 06-08, 2008, Wilderness, South Africa
Tobias Blechmann , Christel Baier, Checking Equivalence for Reo Networks, Electronic Notes in Theoretical Computer Science (ENTCS), 215, p.209-226, June, 2008
Pablo Moreno-Ger , Rubén Fuentes-Fernández , José-Luis Sierra-Rodríguez , Baltasar Fernández-Manjón, Original papers: Model-checking for adventure videogames, Information and Software Technology, v.51 n.3, p.564-580, March, 2009
Michael Roberson , Melanie Harries , Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of soundness of type systems, ACM SIGPLAN Notices, v.43 n.10, September 2008
Alper Sen , Vijay K. Garg, Formal Verification of Simulation Traces Using Computation Slicing, IEEE Transactions on Computers, v.56 n.4, p.511-527, April 2007
Andrea Fedeli , Franco Fummi , Graziano Pravadelli, Properties Incompleteness Evaluation by Functional Verification, IEEE Transactions on Computers, v.56 n.4, p.528-544, April 2007
Shoham Ben-David , Dana Fisman , Sitvanit Ruah, Embedding finite automata within regular expressions, Theoretical Computer Science, v.404 n.3, p.202-218, September, 2008
Joao Marques-Silva, Model checking with Boolean Satisfiability, Journal of Algorithms, v.63 n.1-3, p.3-16, January, 2008
Fang Yu , Chao Wang , Aarti Gupta , Tevfik Bultan, Modular verification of web services using efficient symbolic encoding and summarization, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
Konstantinos Aisopos , Chien-Chun Chou , Li-Shiuan Peh, Extending open core protocol to support system-level cache coherence, Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis, October 19-24, 2008, Atlanta, GA, USA
Qingwei Wu , Michael S. Hsiao, A New Simulation-Based Property Checking Algorithm Based on Partitioned Alternative Search Space Traversal, IEEE Transactions on Computers, v.55 n.11, p.1325-1334, November 2006
Gunjan Khanna , Mike Yu Cheng , Padma Varadharajan , Saurabh Bagchi , Miguel P. Correia , Paulo J. Veríssimo, Automated Rule-Based Diagnosis through a Distributed Monitor System, IEEE Transactions on Dependable and Secure Computing, v.4 n.4, p.266-279, October 2007
Malay K. Ganai , Aarti Gupta, Completeness in SMT-based BMC for software programs, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany
Mark Reith , Jianwei Niu , William H. Winsborough, Toward practical analysis for trust management policy, Proceedings of the 4th International Symposium on Information, Computer, and Communications Security, March 10-12, 2009, Sydney, Australia
Alastair F. Donaldson , Alice Miller, Automatic Symmetry Detection for Promela, Journal of Automated Reasoning, v.41 n.3-4, p.251-293, November 2008
Chen-Hsuan Lin , Chun-Yao Wang, Dependent latch identification in the reachable state space, Proceedings of the 2009 Conference on Asia and South Pacific Design Automation, January 19-22, 2009, Yokohama, Japan
Nadia Hamani , Nathalie Dangoumau , Etienne Craye, Verification and validation of a SSM model dedicated to mode handling of flexible manufacturing systems, Computers in Industry, v.60 n.2, p.77-85, February, 2009
Zijiang Yang , Chao Wang , Aarti Gupta , Franjo Ivanvčić, Model checking sequential software programs via mixed symbolic analysis, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.14 n.1, p.1-26, January 2009
Robert M. Hierons , Kirill Bogdanov , Jonathan P. Bowen , Rance Cleaveland , John Derrick , Jeremy Dick , Marian Gheorghe , Mark Harman , Kalpesh Kapoor , Paul Krause , Gerald Lüttgen , Anthony J. H. Simons , Sergiy Vilkomir , Martin R. Woodward , Hussein Zedan, Using formal specifications to support testing, ACM Computing Surveys (CSUR), v.41 n.2, p.1-76, February 2009
Wojciech Penczek , Maciej Szreter, SAT-based Unbounded Model Checking of Timed Automata, Fundamenta Informaticae, v.85 n.1-4, p.425-440, September 2008
Zhi-Hong Tao , Cong-Hua Zhou , Zhong Chen , Li-Fu Wang, Bounded model checking of CTL, Journal of Computer Science and Technology, v.22 n.1, p.39-43, January 2007
Zhi-Hong Tao , Hans Kleine Büning , Li-Fu Wang, Direct model checking matrix algorithm, Journal of Computer Science and Technology, v.21 n.6, p.944-949, November 2006
Andrzej Zbrzezny , Bożena Woźna, Towards Verification of Java Programs in perICS, Fundamenta Informaticae, v.85 n.1-4, p.533-548, September 2008
James Slagle , Subash Shankar, Theorem proving, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
K. L. McMillan, Model checking, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
Jewgenij Botaschanjan , Benjamin Hummel, Specifying the worst case: orthogonal modeling of hardware errors, Proceedings of the eighteenth international symposium on Software testing and analysis, July 19-23, 2009, Chicago, IL, USA
Mehdi Mohammadi , Hossein Pazhoumand-dar , Mohsen Soryani , Hossein Moeinzadeh, HS-ROBDD: an efficient variable order binary decision diagram, Proceedings of the 11th annual conference companion on Genetic and evolutionary computation conference, July 08-12, 2009, Montreal, Québec, Canada
Robert Brummayer , Armin Biere , Florian Lonsing, BTOR: bit-precise modelling of word-level problems for model checking, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, July 07-14, 2008, Princeton, New Jersey
Bing Li , Chris Ka-Kei Kwok, Automatic formal verification of clock domain crossing signals, Proceedings of the 2009 Conference on Asia and South Pacific Design Automation, January 19-22, 2009, Yokohama, Japan
Natarajan Shankar, Automated deduction for verification, ACM Computing Surveys (CSUR), v.41 n.4, p.1-56, October 2009
Kaile Su, Model checking temporal logics of knowledge in distributed systems, Proceedings of the 19th national conference on Artifical intelligence, p.98-103, July 25-29, 2004, San Jose, California
J. Julliand , P. -A. Masson , E. Oudot, Partitioned PLTL model-checking for refined transition systems, Information and Computation, v.207 n.6, p.681-698, June, 2009
Kazuhiro Ogata , Kokichi Futatsugi, Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, v.E90-A n.8, p.1690-1703, August 2007
F. Belardinelli , A. Lomuscio, Quantified epistemic logics for reasoning about knowledge in multi-agent systems, Artificial Intelligence, v.173 n.9-10, p.982-1013, June, 2009
Sascha Klüppelholz , Christel Baier, Symbolic model checking for channel-based component connectors, Science of Computer Programming, v.74 n.9, p.688-701, July, 2009
Sara Kalvala , Richard Warburton , David Lacey, Program transformations using temporal logic side conditions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.4, p.1-48, May 2009
Gunjan Khanna , Padma Varadharajan , Saurabh Bagchi, Automated Online Monitoring of Distributed Applications through External Monitors, IEEE Transactions on Dependable and Secure Computing, v.3 n.2, p.115-129, April 2006
Artur Rataj , Bożena Woźna , Andrzej Zbrzezny, A Translator of Java Programs to TADDs, Fundamenta Informaticae, v.93 n.1-3, p.305-324, January 2009
Hong Liu , David P. Gluch, Formal verification of AADL behavior models: a feasibility investigation, Proceedings of the 47th Annual Southeast Regional Conference, March 19-21, 2009, Clemson, South Carolina
Alexei Sharpanskykh , Jan Treur, Verifying Interlevel Relations within Multi-Agent Systems, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.290-294, May 22, 2006
Jussi Rintanen, A New Approach to Planning in Networks, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.917-918, June 27, 2008
Sa'ed Abed , Otmane Ait Mohamed , Ghiath Al-Sammane, An abstract reachability approach by combining HOL induction and multiway decision graphs, Journal of Computer Science and Technology, v.24 n.1, p.76-95, January 2009
Stefan Edelkamp, Taming numbers and durations in the model checking integrated planning system, Journal of Artificial Intelligence Research, v.20 n.1, p.195-238, December 2003
Rune M. Jensen , Manuela M. Veloso, OBDD-based universal planning for synchronized agents in non-deterministic domains, Journal of Artificial Intelligence Research, v.13 n.1, p.189-226, August 2000
Jinbo Huang , Adnan Darwiche, The language of search, Journal of Artificial Intelligence Research, v.29 n.1, p.191-219, May 2007
Orna Grumberg , Shlomi Livne , Shaul Markovitch, Learning to order BDD variables in verification, Journal of Artificial Intelligence Research, v.18 n.1, p.83-116, January 2003
Alessandro Cimatti , Marco Roveri, Conformant planning via symbolic model checking, Journal of Artificial Intelligence Research, v.13 n.1, p.305-338, August 2000
Chenggang Wang , Saket Joshi , Roni Khardon, First order decision diagrams for relational MDPs, Journal of Artificial Intelligence Research, v.31 n.1, p.431-472, January 2008
Robert Mateescu , Rina Dechter , Radu Marinescu, AND/OR multi-valued decision diagrams (AOMDDs) for graphical models, Journal of Artificial Intelligence Research, v.33 n.1, p.465-519, September 2008
Hideaki Nishihara , Koichi Shinozaki , Koji Hayamizu , Toshiaki Aoki , Kenji Taguchi , Fumihiro Kumeno, Model checking education for software engineers in Japan, ACM SIGCSE Bulletin, v.41 n.2, June 2009
Yasuyuki Tahara , Nobukazu Yoshioka , Kenji Taguchi , Toshiaki Aoki , Shinichi Honiden, Evolution of a course on model checking for practical applications, ACM SIGCSE Bulletin, v.41 n.2, June 2009
Alessandro Cimatti , Charles Pecheur , Roberto Cavada, Formal verification of diagnosability via symbolic model checking, Proceedings of the 18th international joint conference on Artificial intelligence, p.363-369, August 09-15, 2003, Acapulco, Mexico
Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri, Heuristic search + symbolic model checking = efficient conformant planning, Proceedings of the 17th international joint conference on Artificial intelligence, p.467-472, August 04-10, 2001, Seattle, WA, USA
Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Planning in nondeterministic domains under partial observability via symbolic model checking, Proceedings of the 17th international joint conference on Artificial intelligence, p.473-478, August 04-10, 2001, Seattle, WA, USA
A. L. Juarez Dominguez, Feature Interaction Detection in the Automotive Domain, Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, p.521-524, September 15-19, 2008
A. Kuehlmann , A. Srinivasan , D. P. LaPotin, Verity—a formal verification program for custom CMOS circuits, IBM Journal of Research and Development, v.39 n.1-2, p.149-165, Jan./March 1995
T. Schlipf , T. Buechner , R. Fritz , M. Helms , J. Koehl, Formal verification made easy, IBM Journal of Research and Development, v.41 n.4-5, p.567-576, July/Sept. 1997
J. M. Cobleigh , L. A. Clarke , L. J. Osterweil, FLAVERS: a finite state verification technique for software systems, IBM Systems Journal, v.41 n.1, p.140-165, January 2002
Chen-Hsuan Lin , Chun-Yao Wang , Yung-Chih Chen, Dependent-latch identification in reachable state space, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, v.28 n.8, p.1113-1126, August 2009
Dominique Borrione , Amr Helmy , Laurence Pierre , Julien Schmaltz, A formal approach to the verification of networks on chip, EURASIP Journal on Embedded Systems, 2009, p.1-14, January 2009
Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Strong planning under partial observability, Artificial Intelligence, v.170 n.4-5, p.337-384, April, 2006
Younes Lahbib , Romain Kamdem , Mohamed-lyes Benalycherif , Rached Tourki, An automatic ABV methodology enabling PSL assertions across SLD flow for SOCs modeled in SystemC, Computers and Electrical Engineering, v.31 n.4-5, p.282-302, June, 2005
Manfred Droste , George Rahonis, Weighted automata and weighted logics with discounting, Theoretical Computer Science, v.410 n.37, p.3481-3494, September, 2009
Edmund M. Clarke , E. Allen Emerson , Joseph Sifakis, Model checking: algorithmic verification and debugging, Communications of the ACM, v.52 n.11, November 2009
Ranjit Jhala , Rupak Majumdar, Software model checking, ACM Computing Surveys (CSUR), v.41 n.4, p.1-54, October 2009
Ridha Djemal , Mohamed Ayoub Dhouib , Samuel Dellacherie , Rached Tourki, A novel formal verification approach for RTL hardware IP cores, Computer Standards & Interfaces, v.27 n.6, p.637-651, June, 2005
Ramadhana Bramandia , Jiefeng Cheng , Byron Choi , Jeffrey Xu Yu, Optimizing updates of recursive XML views of relations, The VLDB Journal — The International Journal on Very Large Data Bases, v.18 n.6, p.1313-1333, December 2009
Anita Lungu , Pradip Bose , Daniel J. Sorin , Steven German , Geert Janssen, Multicore power management: ensuring robustness via early-stage formal verification, Proceedings of the 7th IEEE/ACM international conference on Formal Methods and Models for Codesign, p.78-87, July 13-15, 2009, Cambridge, Massachusetts
Collaborative Colleagues:
Kenneth L. McMillan: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player