ESP

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ESP: path-sensitive program verification in polynomial time

Full text

Pdf (332 KB)

Source

Conference on Programming Language Design and Implementation archive
Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation table of contents

Berlin, Germany

SESSION: Program Correctness table of contents

Pages: 57 - 68

Year of Publication: 2002

ISBN:1-58113-463-0

Also published in ...

Authors

Manuvir Das	Microsoft Research
Sorin Lerner	University of Washington
Mark Seigle	University of Washington

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 39, Downloads (12 Months): 208, Citation Count: 125

Additional Information:

abstract 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/512529.512538 What is a DOI?

ABSTRACT

In this paper, we present a new algorithm for partial program verification that runs in polynomial time and space. We are interested in checking that a program satisfies a given temporal safety property. Our insight is that by accurately modeling only those branches in a program for which the property-related behavior differs along the arms of the branch, we can design an algorithm that is accurate enough to verify the program with respect to the given property, without paying the potentially exponential cost of full path-sensitive analysis.We have implemented this "property simulation" algorithm as part of a partial verification tool called ESP. We present the results of applying ESP to the problem of verifying the file I/O behavior of a version of the GNU C compiler (gcc, 140,000 LOC). We are able to prove that all of the 646 calls to .fprintf in the source code of gcc are guaranteed to print to valid, open files. Our results show that property simulation scales to large programs and is accurate enough to verify meaningful properties.

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.

	1	Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon [doi>10.1145/503272.503275]
	2	Glenn Ammons , James R. Larus, Improving data-flow analysis with path profiles, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.72-84, June 17-19, 1998, Montreal, Quebec, Canada [doi>10.1145/277650.277665]
	3	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
	4	Rastisalv Bodík , Sadun Anik, Path-sensitive value-flow analysis, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.237-251, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268966]
	5	William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
	6	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]
	7	Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada [doi>10.1145/349299.349309]
	8	M. Das, S. Lerner, and M. Seigle. ESP: Path-Sensitive Program Verification in Polynomial Time. Technical Report MSR-TR-2002-41, Microsoft Corporation, 2002
	9	Manuvir Das , Ben Liblit , Manuel Fähndrich , Jakob Rehof, Estimating the Impact of Scalable Pointer Analysis on Optimization, Proceedings of the 8th International Symposium on Static Analysis, p.260-278, July 16-18, 2001
	10	Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States [doi>10.1145/378795.378811]
	11	D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the sixth USENIX Conference on Operating systems design and implementation, 2000
	12	Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada [doi>10.1145/502034.502041]
	13	David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States [doi>10.1145/231379.231389]
	14	Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany [doi>10.1145/512529.512558]
	15	Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
	16	Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany [doi>10.1145/512529.512539]
	17	C. A. R. Hoare. An axiomatic basis for computer programming. In C. A. R. Hoare and C. B. Jones (Ed.), Essays in Computing Science, Prentice Hall. 1989
	18	L. Holley and B. Rosen. Qualified dataflow analysis. In Conference Record of the Seventh ACM Symposium on Principles of Programming Languages, 1980
	19	Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany [doi>10.1145/512529.512531]
	20	Jens Knoop , Oliver Rüthing , Bernhard Steffen, Expansion-Based Removal of Semantic Partial Redundancies, Proceedings of the 8th International Conference on Compiler Construction, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.91-106, March 22-28, 1999
	21	Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon [doi>10.1145/503272.503276]
	22	Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
	23	Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
	24	Bernhard Steffen, Property-Oriented Expansion, Proceedings of the Third International Symposium on Static Analysis, p.22-41, September 24-26, 1996
	25	R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
	26	Peng Tu , David Padua, Gated SSA-based demand-driven symbolic analysis for parallelizing compilers, Proceedings of the 9th international conference on Supercomputing, p.414-423, July 03-07, 1995, Barcelona, Spain [doi>10.1145/224538.224648]
	27	Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States [doi>10.1145/207110.207111]

CITED BY 125

	Viktor Kuncak , Martin Rinard, Existential heap abstraction entailment is undecidable, Proceedings of the 10th international conference on Static analysis, June 11-13, 2003, San Diego, CA, USA
	John Field , Deepak Goyal , G. Ramalingam , Eran Yahav, Typestate verification: abstraction techniques and complexity results, Proceedings of the 10th international conference on Static analysis, June 11-13, 2003, San Diego, CA, USA
	Ran Shaham , Eran Yahav , Elliot K. Kolodner , Mooly Sagiv, Establishing local temporal heap safety properties with applications to compile-time memory management, Proceedings of the 10th international conference on Static analysis, June 11-13, 2003, San Diego, CA, USA
	Samuel Z. Guyer , Calvin Lin, Client-driven pointer analysis, Proceedings of the 10th international conference on Static analysis, June 11-13, 2003, San Diego, CA, USA
	Ted Kremenek , Dawson Engler, Z-ranking: using statistical analysis to counter the impact of static analysis approximations, Proceedings of the 10th international conference on Static analysis, June 11-13, 2003, San Diego, CA, USA
	Shaunak Chatterjee , Shuvendu K. Lahiri , Shaz Qadeer , Zvonimir Rakamaric, A reachability predicate for analyzing low-level software, Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems, March 24-April 01, 2007, Braga, Portugal
	Naoki Kobayashi, Time regions and effects for resource usage analysis, ACM SIGPLAN Notices, v.38 n.3, March 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
	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
	Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, ACM SIGPLAN Notices, v.37 n.5, May 2002
	Brian Demsky , Martin Rinard, Automatic detection and repair of errors in data structures, ACM SIGPLAN Notices, v.38 n.11, November 2003
	Emmanuel Geay , Eran Yahav , Stephen Fink, Continuous code-quality assurance with SAFE, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Benjamin Chelf , Dawson Engler , Seth Hallem, How to write system-specific, static checkers in metal, ACM SIGSOFT Software Engineering Notes, v.28 n.1, p.51-60, January 2003
	Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, ACM SIGPLAN Notices, v.38 n.5, May 2003
	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
	Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, ACM SIGPLAN Notices, v.39 n.1, p.232-244, January 2004
	Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
	Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, ACM SIGPLAN Notices, v.39 n.1, p.245-255, January 2004
	Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Roman Manevich , Manu Sridharan , Stephen Adams , Manuvir Das , Zhe Yang, PSE: explaining program failures via postmortem static analysis, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM SIGPLAN Notices, v.39 n.4, April 2004
	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
	Glenn Ammons , James R. Larus, Improving data-flow analysis with path profiles, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA
	Yanhong A. Liu , Tom Rothamel , Fuxiang Yu , Scott D. Stoller , Nanjun Hu, Parametric regular path queries, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Brian Chess , Gary McGraw, Static Analysis for Security, IEEE Security and Privacy, v.2 n.6, p.76-79, November 2004
	Ganesh Sittampalam , Oege de Moor , Ken Friis Larsen, Incremental execution of transformation specifications, ACM SIGPLAN Notices, v.39 n.1, p.26-38, January 2004
	Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Darrell Reimer , Edith Schonberg , Kavitha Srinivas , Harini Srinivasan , Bowen Alpern , Robert D. Johnson , Aaron Kershenbaum , Larry Koved, SABER: smart analysis based error reduction, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Trent Jaeger , Antony Edwards , Xiaolan Zhang, Consistency analysis of authorization hook placement in the Linux security modules framework, ACM Transactions on Information and System Security (TISSEC), v.7 n.2, p.175-205, May 2004
	Westley Weimer , George C. Necula, Finding and preventing run-time error handling mistakes, ACM SIGPLAN Notices, v.39 n.10, October 2004
	Ted Kremenek , Ken Ashcraft , Junfeng Yang , Dawson Engler, Correlation exploitation in error ranking, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Hao Chen , Jonathan S. Shapiro, Using build-integrated static checking to preserve correctness invariants, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA
	Darrell Reimer , Edith Schonberg , Kavitha Srinivas , Harini Srinivasan , Julian Dolby , Aaron Kershenbaum , Larry Koved, Validating structural properties of nested objects, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
	Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, ACM SIGPLAN Notices, v.40 n.1, p.310-323, January 2005
	Corneliu Popeea , Wei-Ngan Chin, A type system for resource protocol verification and its correctness proof, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.135-146, August 24-25, 2004, Verona, Italy
	Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, ACM SIGPLAN Notices, v.40 n.1, p.351-363, January 2005
	David Hovemeyer , William Pugh, Finding bugs is easy, ACM SIGPLAN Notices, v.39 n.12, December 2004
	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.264-313, March 2005
	Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
	Steven P. Reiss, Specifying and checking component usage, Proceedings of the sixth international symposium on Automated analysis-driven debugging, p.13-22, September 19-21, 2005, Monterey, California, USA
	Ranjit Jhala , Rupak Majumdar, Path slicing, ACM SIGPLAN Notices, v.40 n.6, June 2005
	Thomas Reps , Gogul Balakrishnan , Junghee Lim, Intermediate-representation recovery from low-level code, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Samuel Z. Guyer , Calvin Lin, Error checking with client-driven pointer analysis, Science of Computer Programming, v.58 n.1-2, p.83-114, October 2005
	Martin Rinard , Cristian Cadar , Huu Hai Nguyen, Exploring the acceptability envelope, Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	David Hovemeyer , Jaime Spacco , William Pugh, Evaluating and tuning a static analysis to find null pointer bugs, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
	Hari Hampapuram , Yue Yang , Manuvir Das, Symbolic path simulation in path-sensitive dataflow analysis, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
	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
	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
	Jeffrey Fischer , Ranjit Jhala , Rupak Majumdar, Joining dataflow with predicates, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
	Ran Shaham , Eran Yahav , Elliot K. Kolodner , Mooly Sagiv, Establishing local temporal heap safety properties with applications to compile-time memory management, Science of Computer Programming, v.58 n.1-2, p.264-289, October 2005
	Lingxiao Jiang , Zhendong Su, Osprey: a practical type system for validating dimensional unit correctness of C programs, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Dinakar Dhurjati , Sumant Kowshik , Vikram Adve, SAFECode: enforcing alias analysis for weakly typed languages, ACM SIGPLAN Notices, v.41 n.6, June 2006
	Brian Demsky , Michael D. Ernst , Philip J. Guo , Stephen McCamant , Jeff H. Perkins , Martin Rinard, Inference and enforcement of data structure consistency specifications, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	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
	Xiaolan Zhang , Larry Koved , Marco Pistoia , Sam Weber , Trent Jaeger , Guillaume Marceau , Liangzhao Zeng, The case for analysis preserving language transformation, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	Diomidis Spinellis , Panagiotis Louridas, A framework for the static verification of api calls, Journal of Systems and Software, v.80 n.7, p.1156-1168, July, 2007
	Raymond P.L. Buse , Westley R. Weimer, Automatic documentation inference for exceptions, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
	Stephen J. Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008
	Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	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
	Westley Weimer, Patches as better bug reports, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	Nic Volanschi, Condate: a proto-language at the confluence between checking and compiling, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
	Magiel Bruntink , Arie van Deursen , Tom Tourwé, Discovering faults in idiom-based exception handling, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Ghassan Misherghi , Zhendong Su, HDD: hierarchical delta debugging, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Vibha Singhal Sinha , Saurabh Sinha , Swathi Rao, BUGINNINGS: identifying the origins of a bug, Proceedings of the 3rd India software engineering conference, February 25-27, 2010, Mysore, India
	Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006
	Ranjit Jhala , Rupak Majumdar, Bit level types for high level reasoning, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
	Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, ACM SIGPLAN Notices, v.42 n.1, January 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
	Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , Abdullah Ustuner, Thorough static analysis of device drivers, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
	Michael F. Spear , Tom Roeder , Orion Hodson , Galen C. Hunt , Steven Levi, Solving the starting problem: device drivers as self-describing artifacts, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
	Wei Le , Mary Lou Soffa, Refining buffer overflow detection via demand-driven path-sensitive analysis, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.63-68, June 13-14, 2007, San Diego, California, USA
	Eric Brewer , Jeremy Condit , Bill McCloskey , Feng Zhou, Thirty years is long enough: getting beyond C, Proceedings of the 10th conference on Hot Topics in Operating Systems, p.14-14, June 12-15, 2005, Santa Fe, NM
	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
	Guoqing Xu , Atanas Rountev, AJANA: a general framework for source-code-level interprocedural dataflow analysis of AspectJ software, Proceedings of the 7th international conference on Aspect-oriented software development, March 31-April 04, 2008, Brussels, Belgium
	Xavier Rival , Laurent Mauborgne, The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.26-es, August 2007
	Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , Dawson Engler, From uncertainty to belief: inferring the specification within, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
	Sigmund Cherem , Lonnie Princehouse , Radu Rugina, Practical memory leak detection using guarded value-flow analysis, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Lingxiao Jiang , Zhendong Su , Edwin Chiu, Context-based detection of clone-related bugs, 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
	Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007
	Thomas Reps , Gogul Balakrishnan, Improved memory-access analysis for x86 executables, Proceedings of the Joint European Conferences on Theory and Practice of Software 17th international conference on Compiler construction, March 29-April 06, 2008, Budapest, Hungary
	Gogul Balakrishnan , Thomas Reps, Analyzing stripped device-driver executables, Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, March 29-April 06, 2008, Budapest, Hungary
	Manu Sridharan , Stephen J. Fink , Rastislav Bodik, Thin slicing, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Isil Dillig , Thomas Dillig , Alex Aiken, Static error detection using semantic inconsistency inference, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Martin T. Vechev , Eran Yahav , David F. Bacon , Noam Rinetzky, CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors, ACM SIGPLAN Notices, v.42 n.6, June 2007
	M. Pistoia , S. Chandra , S. J. Fink , E. Yahav, A survey of static analysis methods for identifying security vulnerabilities in software systems, IBM Systems Journal, v.46 n.2, p.265-288, April 2007
	Dipanwita Sarkar , Muthu Jagannathan , Jay Thiagarajan , Ramanathan Venkatapathy, Flow-insensitive static analysis for detecting integer anomalies in programs, Proceedings of the 25th conference on IASTED International Multi-Conference: Software Engineering, p.334-340, February 13-15, 2007, Innsbruck, Austria
	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
	Xi Wang , Zhilei Xu , Xuezheng Liu , Zhenyu Guo , Xiaoge Wang , Zheng Zhang, Conditional correlation analysis for safe region-based memory management, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Steven P. Reiss, Incremental Maintenance of Software Artifacts, IEEE Transactions on Software Engineering, v.32 n.9, p.682-697, September 2006
	Greta Yorsh , Eran Yahav , Satish Chandra, Generating precise and concise procedure summaries, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Mark Gabel , Zhendong Su, Symbolic mining of temporal specifications, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Xi Wang , Zhenyu Guo , Xuezheng Liu , Zhilei Xu , Haoxiang Lin , Xiaoge Wang , Zheng Zhang, Hang analysis: fighting responsiveness bugs, ACM SIGOPS Operating Systems Review, v.42 n.4, May 2008
	Jan Wen Voung , Ranjit Jhala , Sorin Lerner, RELAY: static race detection on millions of lines of code, 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
	Prakash Chandrasekaran , Christopher L. Conway , Joseph M. Joy , Sriram K. Rajamani, Programming asynchronous layers with CLARITY, 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
	Aditya Thakur , R. Govindarajan, Comprehensive path-sensitive data-flow analysis, Proceedings of the sixth annual IEEE/ACM international symposium on Code generation and optimization, April 05-09, 2008, Boston, MA, USA
	Nic Volanschi , Christian Rinderknecht, Unparsed patterns: easy user-extensibility of program manipulation tools, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, 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
	Westley Weimer , George C. Necula, Exceptional situations and program reliability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.2, p.1-51, March 2008
	Christian Skalka , Scott Smith , David Van horn, Types and trace effects of higher order programs, Journal of Functional Programming, v.18 n.2, p.179-249, March 2008
	Eric Larson, Assessing work for static software bug detection, Proceedings of the 1st ACM international workshop on Empirical assessment of software engineering languages and technologies: held in conjunction with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE) 2007, p.7-12, November 05-05, 2007, Atlanta, Georgia
	Cristina Cifuentes , Bernhard Scholz, Parfait: designing a scalable bug checker, Proceedings of the 2008 workshop on Static analysis, p.4-11, June 12-12, 2008, Tucson, Arizona
	Isil Dillig , Thomas Dillig , Alex Aiken, Sound, complete and scalable path-sensitive analysis, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Nupur Kothari , Todd Millstein , Ramesh Govindan, Deriving State Machines from TinyOS Programs Using Symbolic Execution, Proceedings of the 7th international conference on Information processing in sensor networks, p.271-282, April 22-24, 2008
	Mark Gabel , Zhendong Su, Javert: fully automatic mining of general temporal properties from dynamic traces, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	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
	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
	Andreas Lochbihler , Gregor Snelting, On temporal path conditions in dependence graphs, Automated Software Engineering, v.16 n.2, p.263-290, June 2009
	Jim Woodcock , Peter Gorm Larsen , Juan Bicarregui , John Fitzgerald, Formal methods: Practice and experience, ACM Computing Surveys (CSUR), v.41 n.4, p.1-36, October 2009
	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
	Gürcan GüleşIr , Klaas Berg , Lodewijk Bergmans , Mehmet Akşit, Experimental evaluation of a tool for the verification and transformation of source code in event-driven systems, Empirical Software Engineering, v.14 n.6, p.720-777, December 2009
	Siliang Li , Gang Tan, Finding bugs in exceptional situations of JNI programs, Proceedings of the 16th ACM conference on Computer and communications security, November 09-13, 2009, Chicago, Illinois, USA
	Ranjit Jhala , Rupak Majumdar, Software model checking, ACM Computing Surveys (CSUR), v.41 n.4, p.1-54, October 2009
	Bernhard Scholz , Chenyi Zhang , Cristina Cifuentes, User-input dependence analysis via graph reachability, Sun Microsystems, Inc., Mountain View, CA, 2008
	Steven P. Reiss, Checking Event-Based Specifications in Java Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.144 n.3, p.107-132, February, 2006
	William R. Harris , Sriram Sankaranarayanan , Franjo Ivančić , Aarti Gupta, Program analysis via satisfiability modulo path programs, ACM SIGPLAN Notices, v.45 n.1, January 2010
	Patrice Godefroid , Aditya V. Nori , Sriram K. Rajamani , Sai Deep Tetali, Compositional may-must program analysis: unleashing the power of alternation, ACM SIGPLAN Notices, v.45 n.1, January 2010
	Al Bessey , Ken Block , Ben Chelf , Andy Chou , Bryan Fulton , Seth Hallem , Charles Henri-Gros , Asya Kamsky , Scott McPeak , Dawson Engler, A few billion lines of code later: using static analysis to find bugs in the real world, Communications of the ACM, v.53 n.2, February 2010
	Eran Yahav , Mooly Sagiv, Verifying safety properties of concurrent heap-manipulating programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.32 n.5, p.1-50, May 2010
	Mark Gabel , Zhendong Su, Online inference and enforcement of temporal properties, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, May 01-08, 2010, Cape Town, South Africa
	Emina Torlak , Satish Chandra, Effective interprocedural resource leak detection, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, May 01-08, 2010, Cape Town, South Africa
	Aditya V. Nori , Sriram K. Rajamani, An empirical study of optimizations in YOGI, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, May 01-08, 2010, Cape Town, South Africa