|
 ABSTRACT
A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).
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
|
Birkhoff{6}. Lattice theory. Amer. Math. Soc. Col. Pub., XXV, Rev. ed.
|
| |
2
|
Cousot{76}. Static determination of dynamic properties of programs. Programming Symp. Paris. Springer-Verlag Lecture Notes in Comp. Sc. to appear (April).
|
| |
3
|
Cousot{76'}. Static determination of dynamic properties of generalized type unions. Submitted for publication. (Sept.)
|
| |
4
|
Floyd{67}. Assigning meanings to programs. Proc. Symp. in Appl. Math. Vol. 19. Mathematical Aspects of Computer Science, (J. Schwartz, ed.) AMS, Providence, R.I., 19-32.
|
 |
5
|
|
| |
6
|
Carl Hewitt , Peter Bishop , Irene Greif , Brian Smith , Todd Matson , Richard Steiger, Actor induction and meta-evaluation, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.153-168, October 01-03, 1973, Boston, Massachusetts
[doi> 10.1145/512927.512942]
|
| |
7
|
|
| |
8
|
Hoare and Lauer{74}. Consistent and Complementary formal theories of the semantics of programming languages. Acts Inf. 3, 135-153.
|
| |
9
|
Kam and Ullman{75}. Monotone data flow analysis frameworks. TR.169, C.S. Lab., Princeton Univ.
|
| |
10
|
Karr{76}. Affine relationships among variables of a program. Acta Inf. 6, 133-151.
|
| |
11
|
|
| |
12
|
|
| |
13
|
Kleene{52}. Introduction to metamathematics. Van Nostrand, New York.
|
| |
14
|
Ligler{75}. Surface properties of programming language constructs. Int. Symp. on Proving and Improving Programs, (G. Huet and G. Kahn, eds.), IRIA, France.
|
| |
15
|
Mac Neille{37}. Partially ordered sets. Trans. Amer. Math. Soc., 42, 416-460.
|
| |
16
|
|
| |
17
|
Morel and Renvoise{76}. Une méthode globale d'élimination des redondances partielles. Programming Symp. Paris. Springer-Verlag Lecture Notes in Comp. Sc. to appear. (April).
|
| |
18
|
Naur{65}. Checking of operand types in ALGOL compilers, BIT 5, 151-163.
|
| |
19
|
Park{69}. Fixpoint induction and proofs of program properties. Machine Intelligence 5, (B. Meltzer and D. Michie, eds.), Edinburgh U. Press, 59-78.
|
| |
20
|
|
| |
21
|
Scott{71}. The lattice of flow diagrams. Symp. on Semantics of Programming Languages. Springer-Verlag Lecture Notes in Math. (E. Engeler, ed.), Vol. 188.
|
| |
22
|
Scott and Strachey{71}. Towards a mathematical semantics for computer languages. Tech. Mon. PRG-6, Oxford U. Comp. Lab.
|
| |
23
|
|
| |
24
|
Sintzoff{75}. Vérifications d'assertions pour les fonctions utilisables comme valeurs affectant des variables extérieures. Int. Symp. on Proving and Improving Programs, (G. Huet and G. Kahn, eds.). IRIA. France.
|
| |
25
|
Sintzoff{76}. Eliminating blind alleys from backtrack programs. Proc. of the third Int. Coll. on Automata, Languages and Programming, Edinburgh, (July).
|
| |
26
|
|
| |
27
|
|
| |
28
|
|
| |
29
|
Tarski{55}. A lattice theoretical fixpoint theorem and its applications. Pacific journal of Math. 5, 285-309.
|
| |
30
|
Tenenbaum{74}. Type determination for very high level languages. NSO-3, Courant Inst. of Math. Sc., New York U., (Oct.).
|
| |
31
|
Ullman{75}. Data flow analysis. Tech. Rep. 179, Dep. of Elec. Eng., Comp. Sc. Lab., Princeton U., (March).
|
| |
32
|
Wegbreit{75}. Property extraction in well-founded property sets. IEEE trans. on Soft. Eng., Vol . SE-1, No. 3, (Sept.)
|
| |
33
|
|
CITED BY 601
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Keshav Pingali , Micah Beck , Richard Johnson , Mayan Moudgill , Paul Stodghill, Dependence flow graphs: an algebraic approach to program dependencies, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.67-78, January 21-23, 1991, Orlando, Florida, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Roberto Barbuti , Michael Codish , Roberto Giacobazzi , Giorgio Levi, Modelling Prolog control, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.95-104, January 19-22, 1992, Albuquerque, New Mexico, United States
|
|
|
|
|
|
|
|
|
|
|
|
B. E. Hart , S. Danforth , P. Valduriez, Parallelizing a database programming language, Proceedings of the first international symposium on Databases in parallel and distributed systems, p.72-79, December 05-07, 1988, Austin, Texas, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Rajnish Ghughal , Abdel Mokkedem , Ratan Nalumasu , Ganesh Gopalakrishnan, Using “test model-checking” to verify the Runway-PA8000 memory model, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.231-239, June 28-July 02, 1998, Puerto Vallarta, Mexico
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
M. Codish , A. Mulkers , M. Bruynooghe , M. García de la Banda , M. Hermenegildo, Improving abstract interpretations by combining domains, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.194-205, June 14-16, 1993, Copenhagen, Denmark
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Frédéric Besson , Thomas de Grenier de Latour , Thomas Jensen, Secure calling contexts for stack inspection, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.76-87, October 06-08, 2002, Pittsburgh, PA, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Patrick Cousot , Radhia Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.83-94, January 19-22, 1992, Albuquerque, New Mexico, United States
|
|
|
|
|
|
|
|
|
James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland
|
|
|
|
|
|
|
|
|
Roberto Bagnara , Enea Zaffanella , Patricia M. Hill, Enhanced sharing analysis techniques: a comprehensive evaluation, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.103-114, September 20-23, 2000, Montreal, Quebec, Canada
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Nevin Heintze , Joxan Jaffar , Răzvan Voicu, A framework for combining analysis and verification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-39, January 19-21, 2000, Boston, MA, USA
|
|
|
M. Garcia de la Banda , M. Hermenegildo , M. Bruynooghe , V. Dumortier , G. Janssens , W. Simoens, Global analysis of constraint logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.5, p.564-614, Sept. 1996
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Roderick Bloem , Kavita Ravi , Fabio Somenzi, Symbolic guided search for CTL model checking, Proceedings of the 37th conference on Design automation, p.29-34, June 05-09, 2000, Los Angeles, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Pei-Hsin Ho , Adrian J. Isles , Timothy Kam, Formal verification of pipeline control using controlled token nets and abstract interpretation, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.529-536, November 08-12, 1998, San Jose, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
C. R. Ramakrishnan , I. V. Ramakrishnan , R. C. Sekar, A symbolic constraint solving framework for analysis of logic programs, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.12-23, June 21-23, 1995, La Jolla, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Byeong-Mo Chang , Kwang-Moo Choe , Roberto Giacobazzi, Abstract filters: improving bottom-up execution of logic programs by two-phase abstract interpretation, Proceedings of the 1994 ACM symposium on Applied computing, p.388-393, March 06-08, 1994, Phoenix, Arizona, United States
|
|
|
Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérôme Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Patrick Cousot , Radhia Cousot, Formal language, grammar and set-constraint-based program analysis by abstract interpretation, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.170-181, June 26-28, 1995, La Jolla, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Stephen Edwards , Luciano Lavagno , Edward A. Lee , Alberto Sangiovanni-Vincentelli, Design of embedded systems: formal models, validation, and synthesis, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Agostino Cortesi , Baudouin Le Charlier , Pascal Van Hentenryck, Combinations of abstract domains for logic programming, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.227-239, January 16-19, 1994, Portland, Oregon, United States
|
|
|
Kim Marriott , María José García de la Banda , Manuel Hermenegildo, Analyzing logic programs with dynamic scheduling, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.240-253, January 16-19, 1994, Portland, Oregon, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Michael Codish , Harald Søndergaard, Meta-circular abstract interpretation in prolog, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
|
|
|
John Hatcliff , Matthew B. Dwyer , Corina S. Păsăreanu , Robby, Foundations of the Bandera abstraction tools, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
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
|
|
|
Saumya Debray , Robert Muth , Matthew Weippert, Alias analysis of executable code, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-24, January 19-21, 1998, San Diego, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Jyh-Herng Chow , William Ludwell Harrison, III, Compile-time analysis of parallel programs that share memory, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 19-22, 1992, Albuquerque, New Mexico, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
William Chan , Richard J. Anderson , Paul Beame , David Notkin , David H. Jones , William E. Warner, Optimizing Symbolic Model Checking for Statecharts, IEEE Transactions on Software Engineering, v.27 n.2, p.170-190, February 2001
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, Type-based verification of sssembly language for compiler debugging, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.91-102, January 10-10, 2005, Long Beach, California, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Hanne Riis Nielson , Flemming Nielson, Flow logic: a multi-paradigmatic approach to static analysis, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Cong Liu , Alex Kondratyev , Yosinori Watanabe , Alberto Sangiovanni-Vincentelli, A structural approach to quasi-static schedulability analysis of communicating concurrent programs, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manuel V. Hermenegildo , Elvira Albert , Pedro López-García , Germán Puebla, Abstraction carrying code and resource-awareness, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.1-11, July 11-13, 2005, Lisbon, Portugal
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manuel V. Hermenegildo , Elvira Albert , Pedro López-García , Germán Puebla, Abstraction carrying code and resource-awareness, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.1-11, July 11-13, 2005, Lisbon, Portugal
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manuel V. Hermenegildo , Germán Puebla , Francisco Bueno , Pedro López-García, Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor), Science of Computer Programming, v.58 n.1-2, p.115-140, October 2005
|
|
|
|
|
|
Tobias Amnell , Gerd Behrmann , Johan Bengtsson , Pedro R. D'Argenio , Alexandre David , Ansgar Fehnker , Thomas Hune , Bertrand Jeannet , Kim G. Larsen , M. Oliver Möller , Paul Pettersson , Carsten Weise , Wang Yi, UPPAAL: now, next, and future, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manuel Carro , José F. Morales , Henk L. Muller , G. Puebla , M. Hermenegildo, High-level languages for small devices: a case study, Proceedings of the 2006 international conference on Compilers, architecture and synthesis for embedded systems, October 22-25, 2006, Seoul, Korea
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Christopher Kruegel , Engin Kirda , Darren Mutz , William Robertson , Giovanni Vigna, Automating mimicry attacks using static binary analysis, Proceedings of the 14th conference on USENIX Security Symposium, p.11-11, July 31-August 05, 2005, Baltimore, MD
|
|
|
María del Mar Gallardo , Jesús Martínez , Pedro Merino , Pablo Nuñez , Ernesto Pimentel, PiXL: Applying xml standards to support the integration of analysis tools for protocols, Science of Computer Programming, v.65 n.1, p.57-69, March, 2007
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Kees van Hee , Olivia Oanea , Alexander Serebrenik , Natalia Sidorova , Marc Voorhoeve, LogLogics: A logic for history-dependent business processes, Science of Computer Programming, v.65 n.1, p.30-40, March, 2007
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sriram Sankaranarayanan , Swarat Chaudhuri , Franjo Ivančić , Aarti Gupta, Dynamic inference of likely data preconditions over predicates by tree learning, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
P. T. Breuer , N. Martinez Madrid , J. P. Bowen , R. France , M. Lorrondo Petrie , C. Delgado Kloos, Reasoning about VHDL and VHDL-AMS using denotational semantics, Proceedings of the conference on Design, automation and test in Europe, p.72-es, January 1999, Munich, Germany
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Glenn Bruns , Daniel S Dantas , Michael Huth, A simple and expressive semantic framework for policy composition in access control, Proceedings of the 2007 ACM workshop on Formal methods in security engineering, p.12-21, November 02-02, 2007, Fairfax, Virginia, USA
|
|
|
|
|
|
|
|
|
Pawel S. Pietrzak , Jesús Correas Fernández , Germán Puebla , Manuel V. Hermenegildo, A practical type analysis for verification of modular prolog programs, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
E. Albert , P. Arenas , S. Genaim , G. Puebla , D. Zanardini, Removing useless variables in cost analysis of Java bytecode, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reinhard Wilhelm , Jakob Engblom , Andreas Ermedahl , Niklas Holsti , Stephan Thesing , David Whalley , Guillem Bernat , Christian Ferdinand , Reinhold Heckmann , Tulika Mitra , Frank Mueller , Isabelle Puaut , Peter Puschner , Jan Staschulat , Per Stenström, The worst-case execution-time problem—overview of methods and survey of tools, ACM Transactions on Embedded Computing Systems (TECS), v.7 n.3, p.1-53, April 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Ti Zhou , Mengjun Li , Zhoujun Li, Local abstract verification and refinement of security protocols, Proceedings of the 6th ACM workshop on Formal methods in security engineering, p.21-30, October 27-27, 2008, Alexandria, Virginia, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Benjamin H. Y. Koo , Willard L. Simmons , Edward F. Crawley, Algebra of systems: a metalanguage for model synthesis and evaluation, IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans, v.39 n.3, p.501-513, May 2009
|
|
|
M. Alba-Castro , M. Alpuente , S. Escobar , P. Ojeda , D. Romero, A Tool for Automated Certification of Java Source Code in Maude, Electronic Notes in Theoretical Computer Science (ENTCS), 248, p.19-29, August, 2009
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf