Dynamically inferring temporal properties

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Dynamically inferring temporal properties

Full text

Pdf (254 KB)

Source

Workshop on Program Analysis for Software Tools and Engineering archive
Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering table of contents

Washington DC, USA

SESSION: Dynamic analysis table of contents

Pages: 23 - 28

Year of Publication: 2004

ISBN:1-58113-910-1

Authors

Jinlin Yang	University of Virginia, Charlottesville, VA
David Evans	University of Virginia, Charlottesville, VA

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 28, Citation Count: 9

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

ABSTRACT

Model checking requires a specification of the target system's desirable properties, some of which are temporal. Formulating a temporal property of the system based on either its abstract model or implementation requires a deep understanding of its behavior and sophisticated knowledge of the chosen formalism. This has been a major impediment to documenting and verifying temporal properties. We propose a dynamic approach to automatically infer a program's temporal properties based on a set of property pattern templates. We describe a preliminary implementation of this approach, and report on our experience using it to discover interesting temporal properties of a small program.

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
	2	Glenn Ammons , David Mandelin , Rastislav Bodík , James R. Larus, Debugging temporal specifications with concept analysis, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
	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	Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
	5	J. E. Cook, Z. Du, C. Liu, and A. L. Wolf. Discovering models of behavior for concurrent systems. New Mexico State University Technical Report, NMSU-CSTR-2002-010.
	6	James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
	7	J. Corbett, M. Dwyer, and J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: the Bandera specification language. KSU CIS Technical Report 2001 -04, Kansas State University, 2001.
	8	Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
	9	Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
	10	Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
	11	Gerard J. Holzmann, The logic of bugs, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587064]
	12	K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. In International Journal on Software Tools for Technology Transfer, September 1999.
	13	Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.245-264, August 30-September 01, 2000
	14	Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
	15	Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
	16	A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, October/November 1977.
	17	John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy

CITED BY 9

	Jeremy S. Bradbury , James R. Cordy , Juergen Dingel, An empirical framework for comparing effectiveness of testing and property-based formal analysis, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
	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
	Valentin Dallmeier , Christian Lindig , Andrzej Wasylkowski , Andreas Zeller, Mining object behavior with ADABU, Proceedings of the 2006 international workshop on Dynamic systems analysis, May 23-23, 2006, Shanghai, China
	Christoph Csallner , Nikolai Tillmann , Yannis Smaragdakis, DySy: dynamic symbolic execution for invariant inference, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Tao Xie , Evan Martin , Hai Yuan, Automatic extraction of abstract-object-state machines from unit-test executions, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	David Evans , Michael Peck, Inculcating invariants in introductory courses, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Sebastian Elbaum , Kalyan-Ram Chilakamarri , Marc Fisher, II , Gregg Rothermel, Web application characterization through directed requests, Proceedings of the 2006 international workshop on Dynamic systems analysis, May 23-23, 2006, Shanghai, China
	Yamini Kannan , Koushik Sen, Universal symbolic execution and its application to likely data structure invariant generation, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
	Fadi Zaraket , Wes Masri, Property based coverage criterion, Proceedings of the 2nd International Workshop on Defects in Large Software Systems: Held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2009), July 19-19, 2009, Chicago, Illinois