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.
Construction of Abstract State Graphs with PVS
Source Lecture Notes In Computer Science; Vol. 1254 archive
Proceedings of the 9th International Conference on Computer Aided Verification table of contents
Pages: 72 - 83  
Year of Publication: 1997
ISBN:3-540-63166-6
Authors
Susanne Graf
Hassen Saïdi
Publisher
Springer-Verlag  London, UK
Bibliometrics
Downloads (6 Weeks): n/a,   Downloads (12 Months): n/a,   Citation Count: 133
Additional Information:

cited by   collaborative colleagues  

Tools and Actions: Review this Article  

CITED BY  134
Bin Chen , George S. Avrunin , Elizabeth A. Henneman , Lori A. Clarke , Leon J. Osterweil , Philip L. Henneman, Analyzing medical processes, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland
Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, ACM SIGPLAN Notices, v.37 n.1, p.58-70, Jan. 2002
Giorgio Delzanno, Constraint-Based Verification of Parameterized Cache Coherence Protocols, Formal Methods in System Design, v.23 n.3, p.257-301, November 2003
Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, v.36 n.5, p.203-213, May 2001
Cormac Flanagan , Stephen N. Freund, Detecting race conditions in large programs, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.90-96, June 2001, Snowbird, Utah, United States
Robert J. Hall, Specification, validation, and synthesis of email agent controllers: A case study in function rich reactive system design, Proceedings of the third workshop on Formal methods in software practice, p.13-23, August 2000, Portland, Oregon, United States
Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, ACM SIGPLAN Notices, v.37 n.1, p.191-202, Jan. 2002
Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, ACM SIGPLAN Notices, v.37 n.1, p.1-3, Jan. 2002
Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, ACM SIGPLAN Notices, v.37 n.5, May 2002
G. Ramalingam , Alex Warshavsky , John Field , Deepak Goyal , Mooly Sagiv, Deriving specialized program analyses for certifying component-client conformance, ACM SIGPLAN Notices, v.37 n.5, May 2002
William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States
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
Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006
Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, ACM SIGPLAN Notices, v.38 n.5, May 2003
B. Jeannet, Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems, Formal Methods in System Design, v.23 n.1, p.5-37, July 2003
John Rushby, Theorem proving for verification, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
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
Marsha Chechik , Benet Devereux , Arie Gurfinkel, Model-checking infinite state-space systems with fine-grained abstractions using SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.16-36, May 2001, Toronto, Ontario, Canada
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
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, ACM SIGPLAN Notices, v.39 n.6, May 2004
Mariya Koshkina , Franck van Breugel, Modelling and verifying web service orchestration by means of the concurrency workbench, ACM SIGSOFT Software Engineering Notes, v.29 n.5, September 2004
Robert A. Riemenschneider , Hassen Saidi , Bruno Dutertre, Using Model Checking to Assess the Dependability of Agent-Based Systems, IEEE Intelligent Systems, v.19 n.5, p.62-70, September 2004
S. Chaki , E. Clarke , A. Groce , J. Ouaknine , O. Strichman , K. Yorav, Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design, v.25 n.2-3, p.129-166, September-November 2004
Sagar Chaki , Alex Groce , Ofer Strichman, Explaining abstract counterexamples, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
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
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
Hassen Saïdi , Bruno Dutertre , Joshua Levy , Alfonso Valdes, Self-regenerative software components, Proceedings of the 2003 ACM workshop on Survivable and self-regenerative systems: in association with 10th ACM Conference on Computer and Communications Security, p.115-120, October 31-31, 2003, Fairfax, VA
Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004
Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, ACM SIGPLAN Notices, v.40 n.1, p.98-109, January 2005
Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, ACM SIGPLAN Notices, v.37 n.5, May 2002
Parosh Aziz Abdulla , Aurore Collomb-Annichini , Ahmed Bouajjani , Bengt Jonsson, Using Forward Reachability Analysis for Verification of Lossy Channel Systems, Formal Methods in System Design, v.25 n.1, p.39-65, July 2004
Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004
Cormac Flanagan, Automatic software model checking via constraint logic, Science of Computer Programming, v.50 n.1-3, p.253-270, March 2004
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Susanne Graf, Characterization of a sequentially consistent memory and verification of a cache memory by abstraction, Distributed Computing, v.12 n.2/3, p.75-90, June 1999
Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Thomas Ball , Todd Millstein , Sriram K. Rajamani, Polymorphic predicate abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.314-343, March 2005
Natarajan Shankar, Automated verification using deduction, exploration, and abstraction, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
G. Parthasarathy , M. K. Iyer , K. T. Cheng , F. Brewer, Structural search for RTL with predicate learning, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Shuvendu K. Lahiri , Shaz Qadeer, Verifying properties of well-founded linked lists, ACM SIGPLAN Notices, v.41 n.1, p.115-126, January 2006
Songtao Xia , Ben Di Vito , César Muñoz, Automated test generation for engineering applications, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
K. L. McMillan, An interpolating theorem prover, Theoretical Computer Science, v.345 n.1, p.101-121, 21 November 2005
Jean-Francois Couchot , Alain Giorgetti , Nikolai Kosmatov, A uniform deductive approach for parameterized protocol safety, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
J. Field , D. Goyal , G. Ramalingam , E. Yahav, Typestate verification: abstraction techniques and complexity results, Science of Computer Programming, v.58 n.1-2, p.57-82, October 2005
Zaher S. Andraus , Mark H. Liffiton , Karem A. Sakallah, Refinement strategies for verification methods based on datapath abstraction, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
Ralph D. Jeffords , Constance L. Heitmeyer, A strategy for efficiently verifying requirements, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
Andreas Podelski , Andrey Rybalchenko, Transition predicate abstraction and fair termination, ACM SIGPLAN Notices, v.40 n.1, p.132-144, January 2005
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
Jeffrey Fischer , Ranjit Jhala , Rupak Majumdar, Joining dataflow with predicates, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Klaus Havelund , Mike Lowry , John Penix, Formal Analysis of a Space-Craft Controller Using SPIN, IEEE Transactions on Software Engineering, v.27 n.8, p.749-765, August 2001
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
Edmund Clarke , Orna Grumberg , Muralidhar Talupur , Dong Wang, Highlevel verification of control intensive systems using predicate abstraction, Formal methods and models for system design: a system level perspective, Kluwer Academic Publishers, Norwell, MA, 2004
Alex Groce , Willem Visser, Model checking Java programs using structural heuristics, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
Hon F. Li , Juergen Rilling , Dhrubajyoti Goswami, Granularity-Driven Dynamic Predicate Slicing Algorithms for Message Passing Systems, Automated Software Engineering, v.11 n.1, p.63-89, January 2004
Rajeev Alur , Thao Dang , Franjo Ivančić, Predicate abstraction for reachability analysis of hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.1, p.152-199, February 2006
Byron Cook , Alexey Gotsman , Andreas Podelski , Andrey Rybalchenko , Moshe Y. Vardi, Proving that programs eventually do something good, ACM SIGPLAN Notices, v.42 n.1, January 2007
Alin Deutsch , Liying Sui , Victor Vianu, Specification and verification of data-driven Web applications, Journal of Computer and System Sciences, v.73 n.3, p.442-474, May, 2007
Deepak Kapur , Rupak Majumdar , Calogero G. Zarba, Interpolation for data structures, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, ACM SIGPLAN Notices, v.41 n.10, October 2006
Greta Yorsh , Thomas Ball , Mooly Sagiv, Testing, abstraction, theorem proving: better together!, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Matthew B. Dwyer , Suzette Person , Sebastian Elbaum, Controlling factors in evaluating path-sensitive error detection techniques, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
Josh Berdine , Aziem Chawdhary , Byron Cook , Dino Distefano , Peter O'Hearn, Variance analyses from invariance analyses, ACM SIGPLAN Notices, v.42 n.1, January 2007
Erika Rice Scherpelz , Sorin Lerner , Craig Chambers, Automatic inference of optimizer flow functions from semantic meanings, ACM SIGPLAN Notices, v.42 n.6, June 2007
Daniel Kroening , Natasha Sharygina, Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Ranjit Jhala , Rupak Majumdar, Interprocedural analysis of asynchronous programs, ACM SIGPLAN Notices, v.42 n.1, January 2007
Sumit Gulwani , Nebojsa Jojic, Program verification as probabilistic inference, ACM SIGPLAN Notices, v.42 n.1, January 2007
Kelvin Ku , Thomas E. Hart , Marsha Chechik , David Lie, A buffer overflow benchmark for software model checkers, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
Hassen Saïdi, Guarded models for intrusion detection, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
Andreas Podelski , Andrey Rybalchenko, Transition predicate abstraction and fair termination, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.15-es, May 2007
Narjes Ben Rajeb , Brahim Nasraoui , Riadh Robbana , Tayssir Touili, Verifying Multithreaded Recursive Programs with Integer Variables, Electronic Notes in Theoretical Computer Science (ENTCS), 239, p.143-154, July, 2009
Roberto Passerone , Jerry R. Burch , Alberto L. Sangiovanni-Vincentelli, Refinement preserving approximations for the design and verification of heterogeneous systems, Formal Methods in System Design, v.31 n.1, p.1-33, August 2007
Niels Lohmann , Peter Massuthe , Christian Stahl , Daniela Weinberg, Analyzing interacting WS-BPEL processes using flexible model generation, Data & Knowledge Engineering, v.64 n.1, p.38-54, January, 2008
Edmund Clarke , Himanshu Jain , Daniel Kroening, Verification of SpecC using predicate abstraction, Formal Methods in System Design, v.30 n.1, p.5-28, February 2007
Sudipta Kundu , Sorin Lerner , Rajesh Gupta, Automated refinement checking of concurrent systems, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Byron Cook , Daniel Kroening , Natasha Sharygina, Verification of Boolean programs with unbounded thread creation, Theoretical Computer Science, v.388 n.1-3, p.227-242, December, 2007
Ajeet Shankar , Rastislav Bodík, DITTO: automatic incrementalization of data structure invariant checks (in Java), ACM SIGPLAN Notices, v.42 n.6, June 2007
Patrick M. Rondon , Ming Kawaguci , Ranjit Jhala, Liquid types, ACM SIGPLAN Notices, v.43 n.6, June 2008
Hassen Saïdi, Logical foundation for static analysis: application to binary static analysis for security, ACM SIGAda Ada Letters, v.XXVIII n.1, p.96-102, April 2008
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
Dirk Beyer , Thomas A. Henzinger , Rupak Majumdar , Andrey Rybalchenko, Path invariants, ACM SIGPLAN Notices, v.42 n.6, June 2007
Mark Grechanik, Finding Errors in Interoperating Components, Proceedings of the Second International Workshop on Incorporating COTS Software into Software Systems: Tools and Techniques, p.3, May 20-26, 2007
D. Kroening , E. Clarke, Checking consistency of C and Verilog using predicate abstraction and induction, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.66-72, November 07-11, 2004
R. E. Bryant , S. K. Rajamani, Verifying properties of hardware and software by predicate abstraction and model checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.437-438, November 07-11, 2004
Matthew B. Dwyer , John Hatcliff , Robby Robby , Corina S. Pasareanu , Willem Visser, Formal Software Analysis Emerging Trends in Software Model Checking, 2007 Future of Software Engineering, p.120-136, May 23-25, 2007
Thanyapat Sakunkonchak , Takeshi Matsumoto , Hiroshi Saito , Satoshi Komatsu , Masahiro Fujita, Equivalence checking in C-based system-level design by sequentializing concurrent behaviors, Proceedings of the third conference on IASTED International Conference: Advances in Computer Science and Technology, p.36-42, 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
Ahmed Bouajjani , Agathe Merceron, Parametric Verification of a Group Membership Algorithm, Theory and Practice of Logic Programming, v.6 n.3, p.321-353, May 2006
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
Robert J. Hall, Specification, Validation, and Synthesis of Email Agent Controllers: A Case Study in Function Rich Reactive System Design, Automated Software Engineering, v.9 n.3, p.233-261, August 2002
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
José Meseguer , Prasanna Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order and Symbolic Computation, v.20 n.1-2, p.123-160, June 2007
Mark Kattenbelt , Marta Kwiatkowska , Gethin Norman , David Parker, Game-Based Probabilistic Predicate Abstraction in PRISM, Electronic Notes in Theoretical Computer Science (ENTCS), v.220 n.3, p.5-21, December, 2008
Shuvendu K. Lahiri , Randal E. Bryant, Predicate abstraction with indexed predicates, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.4-es, December 2007
Thomas Witkowski , Nicolas Blanc , Daniel Kroening , Georg Weissenbacher, Model checking concurrent linux device drivers, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
Sunae Seo , Hongseok Yang , Kwangkeun Yi , Taisook Han, Goal-directed weakening of abstract interpretation results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.39-es, October 2007
Sharon Shoham , Orna Grumberg, A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.1-es, December 2007
Vijay D'Silva , Sampada Sonalkar , S. Ramesh, Existential abstractions for distributed reactive systems via syntactic transformations, Proceedings of the 7th ACM & IEEE international conference on Embedded software, September 30-October 03, 2007, Salzburg, Austria
Daniel Kroening , Sanjit A. Seshia, Formal verification at higher levels of abstraction, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Chao Wang , Hyondeuk Kim , Aarti Gupta, Hybrid CEGAR: combining variable hiding and predicate abstraction, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Paul B. Jackson , Bill J. Ellis , Kathleen Sharp, Using SMT solvers to verify high-integrity programs, Proceedings of the second workshop on Automated formal methods, p.60-68, November 06-06, 2007, Atlanta, Georgia
Nicolas Blanc , Alex Groce , Daniel Kroening, Verifying C++ with STL containers via predicate abstraction, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
Shuvendu Lahiri , Shaz Qadeer, Back to the future: revisiting precise program verification using SMT solvers, ACM SIGPLAN Notices, v.43 n.1, January 2008
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
Sagar Chaki , Edmund Clarke , Natasha Sharygina , Nishant Sinha, Verification of evolving software via component substitutability analysis, Formal Methods in System Design, v.32 n.3, p.235-266, June 2008
Junyan Qian_aff1n2 , Baowen Xu, Formal Verification for C Program, Informatica, v.18 n.2, p.289-304, April 2007
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
Jayanta Bhadra , Magdy S. Abadir , Li-C. Wang , Sandip Ray, A Survey of Hybrid Techniques for Functional Verification, IEEE Design & Test, v.24 n.2, p.112-122, March 2007
Mayur Naik , Jens Palsberg, A type system equivalent to a model checker, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.5, p.1-24, August 2008
Sandip Ray , Rob Sumners, Combining Theorem Proving with Model Checking through Predicate Abstraction, IEEE Design & Test, v.24 n.2, p.132-139, March 2007
Sandip Ray , Rob Sumners, Combining Theorem Proving with Model Checking through Predicate Abstraction, IEEE Design & Test, v.24 n.2, p.132-139, March 2007
Ingo Brückner , Klaus Dräger , Bernd Finkbeiner , Heike Wehrheim, Slicing Abstractions, Fundamenta Informaticae, v.89 n.4, p.369-392, January 2009
Nicolas Blanc , Daniel Kroening, Race analysis for SystemC using model checking, Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, November 10-13, 2008, San Jose, California
Natasha Sharygina , Stefano Tonetta , Aliaksei Tsitovich, The synergy of precise and fast abstractions for program verification, Proceedings of the 2009 ACM symposium on Applied Computing, March 08-12, 2009, Honolulu, Hawaii
Arie Gurfinkel , Sagar Chaki, Combining predicate and numeric abstraction for software model checking, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-9, November 17-20, 2008, Portland, Oregon
Natarajan Shankar, Automated deduction for verification, ACM Computing Surveys (CSUR), v.41 n.4, p.1-56, October 2009
Ashish Tiwari, Abstractions for hybrid systems, Formal Methods in System Design, v.32 n.1, p.57-83, February 2008
Saurabh Srivastava , Sumit Gulwani, Program verification using templates over predicate abstraction, ACM SIGPLAN Notices, v.44 n.6, June 2009
Mika Cohen , Mads Dam , Alessio Lomuscio , Francesco Russo, Abstraction in model checking multi-agent systems, Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, May 10-15, 2009, Budapest, Hungary
Wolfgang Mayer , Markus Stumptner, Better Debugging through More Abstract Observations, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.779-780, May 22, 2006
David A. Schmidt, Abstract Interpretation From a Denotational-semantics Perspective, Electronic Notes in Theoretical Computer Science (ENTCS), 249, p.19-37, August, 2009
Santiago Escobar , José Meseguer , Prasanna Thati, Narrowing and Rewriting Logic: from Foundations to Applications, Electronic Notes in Theoretical Computer Science (ENTCS), 177, p.5-33, June, 2007
Shin Nakajima , Naoyasu Ubayashi , Keiji Hokamura, Runtime monitoring of cross-cutting policy, Proceedings of the 2009 ICSE Workshop on Aspect-Oriented Requirements Engineering and Architecture Design, p.20-24, May 18-18, 2009
Toshifusa Sekizawa , Tatsuhiro Tsuchiya , Tohru Kikuno , Koichi Takahashi, Analyzing the one dimensional Ising model by probabilistic model checking, Proceedings of the IASTED Asian Conference on Modelling and Simulation, October 08-10, 2007, Beijing, CHINA
Hiroshi Unno , Naoki Kobayashi, Dependent type inference with interpolants, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, September 07-09, 2009, Coimbra, Portugal
Tomasz Mazur , Gavin Lowe, Counter Abstraction in the CSP/FDR setting, Electronic Notes in Theoretical Computer Science (ENTCS), v.250 n.1, p.171-186, September, 2009
Rohit Chadha , Mahesh Viswanathan, Deciding branching time properties for asynchronous programs, Theoretical Computer Science, v.410 n.42, p.4169-4179, September, 2009
Ranjit Jhala , Rupak Majumdar, Software model checking, ACM Computing Surveys (CSUR), v.41 n.4, p.1-54, October 2009
Changyan Zhou , Ratnesh Kumar, On identification of input/output extended automata with finite bisimilar quotients, Proceedings of the 2009 conference on American Control Conference, p.5653-5658, June 10-12, 2009, St. Louis, Missouri, USA
Xavier Briand , Bertrand Jeannet, Combining control and data abstraction in the verification of hybrid systems, Proceedings of the 7th IEEE/ACM international conference on Formal Methods and Models for Codesign, p.141-150, July 13-15, 2009, Cambridge, Massachusetts
Sean Safarpour , Andreas Veneris, Automated design debugging with abstraction and refinement, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, v.28 n.10, p.1597-1608, October 2009
Collaborative Colleagues:
Susanne Graf: colleagues
Hassen Saïdi: 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