Model checking for programming languages using VeriSoft

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Model checking for programming languages using VeriSoft

Full text

Pdf (1.10 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

Paris, France

Pages: 174 - 186

Year of Publication: 1997

ISBN:0-89791-853-3

Author

Patrice Godefroid

Lucent Technologies, 1000 E. Warrenville Road, Naperville, IL

Sponsors

L'Ecole des Mines de Paris : L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Ctr Natl de la Recherche Sci :
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 31, Downloads (12 Months): 125, Citation Count: 103

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/263699.263717 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	AHU74	Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
	ASU86	Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
	BCM+90	J.R. Butch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428-439, Philadelphia, June 1990.
	BG96	Bernard Boigelot , Patrice Godefroid, Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.465-478, March 18-22, 1996
	Bry92	Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
	CC77	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	CES86	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	CGH+93	Edmund M. Clarke , Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.15-30, April 26-28, 1993
	CGL92	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
	CMN91	Jong-Deok Choi , Barton P. Miller , Robert H. B. Netzer, Techniques for debugging parallel programs with flowback analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.491-530, Oct. 1991 [doi>10.1145/115372.115324]
	Cor96	James C. Corbett, Constructing abstract models of concurrent real-time software, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.250-260, January 08-10, 1996, San Diego, California, United States
	CPS93	Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
	DDHY92	David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
	FGM+92	Jean-Claude Fernandez , Hubert Garavel , Laurent Mounier , Anne Rasse , Carlos Rodriguez , Joseph Sifakis, A toolbox for the verification of LOTOS programs, Proceedings of the 14th international conference on Software engineering, p.246-259, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143124]
	FHS95	A. R. Flora-Holmquist , M. G. Staskauskas, Formal validation of virtual finite state machines, Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p.122, April 05-08, 1995
	GHP95	Patrice Godefroid , Gerard J. Holzmann , Didier Pirottin, State-space caching revisited, Formal Methods in System Design, v.7 n.3, p.227-241, Nov. 1995 [doi>10.1007/BF01384077]
	God90	Patrice Godefroid, Using Partial Orders to Improve Automatic Verification Methods, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.176-185, June 18-21, 1990
	God96	Patrice Godefroid. Partial-Order Methods .for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996.
	GP93	Patrice Godefroid , Didier Pirottin, Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract), Proceedings of the 5th International Conference on Computer Aided Verification, p.438-449, June 28-July 01, 1993
	GW93	Patrice Godefroid , Pierre Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties, Formal Methods in System Design, v.2 n.2, p.149-164, April 1993 [doi>10.1007/BF01383879]
	HK90	Z. Har'El and R. P. Kurshan. Software for analytical development of communication protocols. ATg_4T Technical Journal, 1990.
	Hol85	G.J. Holzmann. Tracing protocols. A T#T Technical Journal, 64(12):2413-2434, 1985.
	Hol91	Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	JJ91	Claude Jard , Thierry Jéron, Bounded-memory Algorithms for Verification On-the-fly, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.192-202, July 01-04, 1991
	KP92	Shmuel Katz , Doron Peled, Defining conditional independence using collapses, Theoretical Computer Science, v.101 n.2, p.337-359, July 20, 1992 [doi>10.1016/0304-3975(92)90054-J]
	Lam77	L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SF_,-3(2):125-143, 1977.
	LC91	Douglas Long , Lori A. Clarke, Data flow analysis of concurrent systems that use the rendezvous model of synchronization, Proceedings of the symposium on Testing, analysis, and verification, p.21-35, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120810]
	LP85	Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
	Maz86	A Mazurkiewicz, Trace theory, Advances in Petri nets 1986, part II on Petri nets: applications and relationships to other models of concurrency, p.279-324, February 1987, Bad Honnef
	McM93	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	MJ81	Steven S. Muchnick , Neil D. Jones, Program Flow Analysis: Theory and Application, Prentice Hall Professional Technical Reference, 1981
	MP92	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	MR93	Stephen P. Masticola , Barbara G. Ryder, Non-concurrency analysis, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.129-138, May 19-22, 1993, San Diego, California, United States
	Ove81	William T. Overman, Verification of concurrent systems: function and timing, 1981
	Pel93	Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
	QS81	Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
	Rud92	Harry Rudin, Protocol Development Success Stories: Part 1, Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification XII, p.149-160, June 22-25, 1992
	Tay83	Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
	Val91	Antti Valmari, Stubborn sets for reduced state generation, Proceedings on Advances in Petri nets 1990, p.491-515, March 1991
	VW86	M.Y. Vardi and P. Wolper. An automatatheoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986.

CITED BY 103

	Gleb Naumovich , Lori A. Clarke , Jamieson M. Cobleigh, Using partial order techniques to improve performance of data flow analysis based verification, ACM SIGSOFT Software Engineering Notes, v.24 n.5, p.57-65, Sept. 1999
	Sanjeev Kumar , Yitzhak Mandelbaum , Xiang Yu , Kai Li, ESP: a language for programmable devices, ACM SIGPLAN Notices, v.36 n.5, p.309-320, May 2001
	Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, ACM SIGPLAN Notices, v.33 n.5, p.345-357, May 1998
	Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA
	David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA
	Premkumar T. Devanbu , Stuart Stubblebine, Software engineering for security: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.227-239, June 04-11, 2000, Limerick, Ireland
	Leszek Holenderski, A model checking project at Philips research, Proceedings of the 8th international SPIN workshop on Model checking of software, p.288-295, May 2001, Toronto, Ontario, Canada
	Karthikeyan Bhargavan , Satish Chandra , Peter J. McCann , Carl A. Gunter, What packets may come: automata for network monitoring, ACM SIGPLAN Notices, v.36 n.3, p.206-219, March 2001
	Patrice Godefroid , James D. Herbsleb , Lalita Jategaonkar Jagadeesany , Du Li, Ensuring privacy in presence awareness: an automated verification approach, Proceedings of the 2000 ACM conference on Computer supported cooperative work, p.59-68, December 2000, Philadelphia, Pennsylvania, United States
	Zhe Dang , Richard A. Kemmerer, Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems, Proceedings of the 22nd international conference on Software engineering, p.345-354, June 04-11, 2000, Limerick, Ireland
	Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004
	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
	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
	Scott D. Stoller, Domain partitioning for open reactive systems, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	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
	Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	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
	Patrice Godefroid , Lalita J. Jagadeesan , Radha Jagadeesan , Konstantin Läufer, Automated systematic testing for constraint-based interactive services, ACM SIGSOFT Software Engineering Notes, v.25 n.6, p.40-49, Nov. 2000
	Klaus Havelund , Grigore Roşu, An Overview of the Runtime Verification Tool Java PathExplorer, Formal Methods in System Design, v.24 n.2, p.189-215, March 2004
	Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, ACM SIGOPS Operating Systems Review, v.36 n.SI, Winter 2002
	Juergen Dingel, Computer-assisted assume/guarantee reasoning with VeriSoft, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Glenn Ammons , David Mandelin , Rastislav Bodík , James R. Larus, Debugging temporal specifications with concept analysis, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
	Abhik Roychoudhury , Tulika Mitra, Specifying multithreaded Java semantics for program verification, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	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
	Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, ACM SIGPLAN Notices, v.39 n.6, May 2004
	David L. Atkins , Thomas Ball , Glenn Bruns , Kenneth Cox, Mawl: A Domain-Specific Language for Form-Based Services, IEEE Transactions on Software Engineering, v.25 n.3, p.334-346, May 1999
	Juergen Dingel , Hongzhi Liang, Automating comprehensive safety analysis of concurrent programs using verisoft and TXL, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, ACM SIGPLAN Notices, v.40 n.1, p.110-121, January 2005
	Doron Peled , Moshe Y. Vardi , Mihalis Yannakakis, Black box checking, Journal of Automata, Languages and Combinatorics, v.7 n.2, p.225-246, November 2001
	Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, ACM SIGPLAN Notices, v.40 n.6, June 2005
	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
	P. de la Cámara , M. M. Gallardo , P. Merino , D. Sanán, Model checking software with well-defined APIs: the socket case, Proceedings of the 10th international workshop on Formal methods for industrial critical systems, p.17-26, September 05-06, 2005, Lisbon, Portugal
	Sanjeev Kumar , Kai Li, Using model checking to debug device firmware, 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
	Margaret DeLap , Björn Knutsson , Honghui Lu , Oleg Sokolsky , Usa Sammapun , Insup Lee , Christos Tsarouchis, Is runtime verification applicable to cheat detection?, Proceedings of 3rd ACM SIGCOMM workshop on Network and system support for games, August 30-30, 2004, Portland, Oregon, USA
	Sarfraz Khurshid , Yuk Lai Suen, Generalizing symbolic execution to library classes, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
	Willem Visser , Corina S. Păsăreanu , Radek Pelánek, Test input generation for red-black trees using abstraction, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	Colin Blundell , Dimitra Giannakopoulou , Corina S. Pǎsǎreanu, Assume-guarantee testing, ACM SIGSOFT Software Engineering Notes, v.31 n.2, March 2006
	David Coppit , Jinlin Yang , Sarfraz Khurshid , Wei Le , Kevin Sullivan, Software Assurance by Bounded Exhaustive Testing, IEEE Transactions on Software Engineering, v.31 n.4, p.328-339, April 2005
	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
	Felice Balarin , Luciano Lavagno , Claudio Passerone , Alberto Sangiovanni-Vincentelli , Yosinori Watanabe , Guang Yang, Concurrent execution semantics and sequential simulation algorithms for the metropolis meta-model, Proceedings of the tenth international symposium on Hardware/software codesign, May 06-08, 2002, Estes Park, Colorado
	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
	Radu Iosif , Matthew B. Dwyer , John Hatcliff, Translating Java for Multiple Model Checkers: The Bandera Back-End, Formal Methods in System Design, v.26 n.2, p.137-180, March 2005
	Kevin Sullivan , Jinlin Yang , David Coppit , Sarfraz Khurshid , Daniel Jackson, Software assurance by bounded exhaustive testing, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Andreas Griesmayer , Roderick Bloem , Martin Hautzendorfer , Franz Wotawa, Formal verification of control software: a case study, Proceedings of the 18th international conference on Innovations in Applied Artificial Intelligence, p.783-788, June 22-24, 2005, Bari, Italy
	Koushik Sen, Effective random testing of concurrent programs, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Sarvani Vakkalanka , Michael DeLisi , Ganesh Gopalakrishnan , Robert M. Kirby, Scheduling considerations for building dynamic verification tools for MPI, Proceedings of the 6th workshop on Parallel and distributed systems: testing, analysis, and debugging, p.1-6, July 20-21, 2008, Seattle, Washington
	Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
	Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, ACM SIGPLAN Notices, v.41 n.10, October 2006
	Scott D. Stoller , Ernie Cohen, Optimistic synchronization-based state-space reduction, Formal Methods in System Design, v.28 n.3, p.263-289, May 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
	Madanlal Musuvathi , Andy Chou , David L. Dill , Dawson Engler, Model checking system software with CMC, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC, July 01-01, 2002, Saint-Emilion, France
	Willem Visser , Corina S. Pǎsǎreanu , Radek Pelánek, Test input generation for java containers using state matching, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	Saddek Bensalem , Jean-Claude Fernandez , Klaus Havelund , Laurent Mounier, Confirmation of deadlock potentials detected by runtime analysis, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA
	Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , Sriram K. Rajamani, SYNERGY: a new algorithm for property checking, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
	Shriram Krishnamurthi , Kathi Fisler, Foundations of incremental aspect model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.16 n.2, p.7-es, April 2007
	Patrice Godefroid, Compositional dynamic test generation, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), v.24 n.4, p.393-423, November 2006
	Madanlal Musuvathi , Dawson R. Engler, Model checking large network protocol implementations, Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation, p.12-12, March 29-31, 2004, San Francisco, California
	Nick Feamster , Hari Balakrishnan, Detecting BGP configuration faults with static analysis, Proceedings of the 2nd conference on Symposium on Networked Systems Design & Implementation, p.43-56, May 02-04, 2005
	Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.19-19, December 06-08, 2004, San Francisco, CA
	Tong Li , Carla S. Ellis , Alvin R. Lebeck , Daniel J. Sorin, Pulse: a dynamic deadlock detection mechanism using speculative execution, Proceedings of the USENIX Annual Technical Conference 2005 on USENIX Annual Technical Conference, p.3-3, April 10-15, 2005, Anaheim, CA
	Marcelo d'Amorim , Steven Lauterburg , Darko Marinov, Delta execution for efficient state-space exploration of object-oriented programs, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom
	Madanlal Musuvathi , Shaz Qadeer, Fair stateless model checking, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Sudipta Kundu , Malay Ganai , Rajesh Gupta, Partial order reduction for scalable testing of systemC TLM designs, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California
	Robert Palmer , Ganesh Gopalakrishnan , Robert M. Kirby, Semantics driven dynamic partial-order reduction of MPI-based parallel programs, Proceedings of the 2007 ACM workshop on Parallel and distributed systems: testing and debugging, July 09-09, 2007, London, United Kingdom
	Graham Hughes , Tevfik Bultan, Interface grammars for modular software model checking, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom
	Madanlal Musuvathi , Shaz Qadeer, Iterative context bounding for systematic testing of multithreaded programs, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Charles Edwin Killian , James W. Anderson , Ryan Braud , Ranjit Jhala , Amin M. Vahdat, Mace: language support for building distributed systems, ACM SIGPLAN Notices, v.42 n.6, June 2007
	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
	Youssef Hanna , Hridesh Rajan , Wensheng Zhang, Slede: a domain-specific verification framework for sensor network security protocol implementations, Proceedings of the first ACM conference on Wireless network security, March 31-April 02, 2008, Alexandria, VA, USA
	Grigore Roşu , Klaus Havelund, Rewriting-Based Techniques for Runtime Verification, Automated Software Engineering, v.12 n.2, p.151-197, April 2005
	Junfeng Yang , Can Sar , Dawson Engler, EXPLODE: a lightweight, general system for finding serious storage system errors, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
	Bassem Elkarablieh , Darko Marinov , Sarfraz Khurshid, Efficient solving of structural constraints, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
	Corina S. Pǎsǎreanu , Peter C. Mehlitz , David H. Bushnell , Karen Gundy-Burlet , Michael Lowry , Suzette Person , Mark Pape, Combining unit-level symbolic execution and system-level concrete execution for testing nasa software, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
	Radek Pelánek , Václav Rosecký , Pavel Moravec, Complementarity of Error Detection Techniques, Electronic Notes in Theoretical Computer Science (ENTCS), v.220 n.2, p.51-65, December, 2008
	Jun Chen , Steve MacDonald, Towards a better collaboration of static and dynamic analyses for testing concurrent programs, Proceedings of the 6th workshop on Parallel and distributed systems: testing, analysis, and debugging, p.1-9, July 20-21, 2008, Seattle, Washington
	Shan Lu , Soyeon Park , Chongfeng Hu , Xiao Ma , Weihang Jiang , Zhenmin Li , Raluca A. Popa , Yuanyuan Zhou, MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs, ACM SIGOPS Operating Systems Review, v.41 n.6, December 2007
	Bassem Elkarablieh , Sarfraz Khurshid , Duy Vu , Kathryn S. McKinley, Starc: static analysis for efficient repair of complex data, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Ganesh Gopalakrishnan , Robert M. Kirby, Formal Methods for MPI Programs, Electronic Notes in Theoretical Computer Science (ENTCS), 193, p.19-27, November, 2007
	Jun Chen , Steve MacDonald, Testing concurrent programs using value schedules, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Azadeh Farzan , José Meseguer, Partial Order Reduction for Rewriting Semantics of Programming Languages, Electronic Notes in Theoretical Computer Science (ENTCS), v.176 n.4, p.61-78, July, 2007
	Sarvani S. Vakkalanka , Subodh Sharma , Ganesh Gopalakrishnan , Robert M. Kirby, ISP: a tool for model checking MPI programs, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, February 20-23, 2008, Salt Lake City, UT, USA
	Octavian Udrea , Cristian Lumezanu , Jeffrey S. Foster, Rule-based static analysis of network protocol implementations, Information and Computation, v.206 n.2-4, p.130-157, February, 2008
	Elliot Barlas , Tevfik Bultan, Netstub: a framework for verification of distributed java applications, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Youssef Hanna, SLEDE: lightweight verification of sensor network security protocol implementations, The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers, September 03-07, 2007, Dubrovnik, Croatia
	Scott D. Fleming , Eileen Kraemer , R. E. K. Stirewalt , Shaohua Xie , Laura K. Dillon, A study of student strategies for the corrective maintenance of concurrent software, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Youssef Hanna, SLEDE: lightweight verification of sensor network security protocol implementations, 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
	Shan Lu , Soyeon Park , Eunsoo Seo , Yuanyuan Zhou, Learning from mistakes: a comprehensive study on real world concurrency bug characteristics, ACM SIGPLAN Notices, v.43 n.3, March 2008
	Chang-Seo Park , Koushik Sen, Randomized active atomicity violation detection in concurrent programs, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Koushik Sen, Race directed random testing of concurrent programs, ACM SIGPLAN Notices, v.43 n.6, June 2008
	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
	Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: Automatically Generating Inputs of Death, ACM Transactions on Information and System Security (TISSEC), v.12 n.2, p.1-38, December 2008
	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
	Hector Miguel Chavez , Wuwei Shen , Shaoying Liu, An approach to detection of UML-based ownership violation, Proceedings of the 2009 ACM symposium on Applied Computing, March 08-12, 2009, Honolulu, Hawaii
	Hector Miguel Chavez , Wuwei Shen, Finding inconsistency for UML-based composition at program level, Proceedings of the 2009 ICSE Workshop on Modeling in Software Engineering, p.32-37, May 17-18, 2009
	Danhua Shao , Sarfraz Khurshid , Dewayne E. Perry, Whispec: white-box testing of libraries using declarative specifications, Proceedings of the 2007 Symposium on Library-Centric Software Design, p.11-20, October 21-21, 2007, Montreal, Canada
	Junfeng Yang , Tisheng Chen , Ming Wu , Zhilei Xu , Xuezheng Liu , Haoxiang Lin , Mao Yang , Fan Long , Lintao Zhang , Lidong Zhou, MODIST: transparent model checking of unmodified distributed systems, Proceedings of the 6th USENIX symposium on Networked systems design and implementation, p.213-228, April 22-24, 2009, Boston, Massachusetts
	Pallavi Joshi , Chang-Seo Park , Koushik Sen , Mayur Naik, A randomized dynamic program analysis technique for detecting real deadlocks, ACM SIGPLAN Notices, v.44 n.6, June 2009