, Compilers, Principles Techniques and Tools, 1986.
, The KeY Tool. Software and System Modeling, vol.4, pp.32-54, 2005.
Termination Analysis of Java Bytecode, Proc. of the 9th International Workshop on Termination (WST'07), 2007. ,
Termination Analysis of Java Bytecode, Proc. of the International Conference on Formal Methods for Open ObjectBased Distributed Systems (FMOODS'08, vol.5051, pp.2-18, 2008. ,
Cost Analysis of Java Bytecode, Proc. of the 16th European Symposium on Programming, vol.4421, pp.157-172, 2007. ,
Size-change Termination and Bound Analysis, Proc. of the 8th International Symposium on Functional and Logic Programming (FLOPS'06, vol.3945, pp.192-207, 2006. ,
Proving Termination by Divergence, Proc. of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM'07), pp.93-102, 2007. ,
Fast Static Analysis of C++ Virtual Function Calls, Proc. of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'96), vol.31, pp.324-341, 1996. ,
Precise Widening Operators for Convex Polyhedra, Science of Computer Programming, vol.58, pp.28-56, 2005. ,
The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems, Science of Computer Programming, vol.72, pp.1-2, 2008. ,
A Program Logic for Bytecode, Electronic Notes on Theoretical Computer Science, vol.141, pp.255-273, 2005. ,
Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Proc. of the 4th International Symposium on Formal Methods for Components and Objects (FMCO'05), vol.4111, pp.364-387, 2005. ,
Program Termination Analysis in Polynomial Time, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, p.1, 2007. ,
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming, Proc. of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'05, vol.3385, pp.1-24, 2007. ,
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Proc. of the 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'77, pp.238-252, 1977. ,
Systematic Design of Program Analysis Frameworks, Proc. of the 6th ACM Symposium on Principles of Programming Languages (POPL'79), pp.269-282, 1979. ,
Automatic Discovery of Linear Restraints among Variables of a Program, Proc. of the 5th ACM Symposium on Principles of Programming Languages (POPL'78), pp.84-96, 1978. ,
Termination of Logic Programs: The Never-Ending Story, Journal of Logic Programming, vol.19, pp.199-260, 1994. ,
Optimization of Object-Oriented Programs using Static Class Hierarchy Analysis, Proc. of the 9th European Conference on Object-Oriented Programming, vol.952, pp.77-101, 1995. ,
A General Framework for Automatic Termination Analysis of Logic Programs. Applicable Algebra in Engineering, Communication and Computing, vol.12, issue.2, pp.117-156, 2001. ,
A Local Shape Analysis Based on Separation Logic, Proc. of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06, vol.3920, pp.287-302, 2006. ,
Assigning Meanings to Programs, Mathematical Aspects of Computer Science, vol.19, pp.19-32, 1967. ,
Goal Independency and Call Patterns in the Analysis of Logic Programs, Proc. of the ACM Symposium on Applied Computing (SAC'94), pp.394-399, 1994. ,
Inferring Termination Conditions for Logic Programs using Backwards Analysis, Theory and Practice of Logic Programming (TPLP), vol.5, pp.75-91, 2005. ,
, Proc. of the 10th Workshop on Formal Techniques for Java-like Programs (FTfJP'08), M. Huisman, 2008.
Automatic Termination Proofs in the Dependency Pair Framework, 3th International Joint Conference on Automated Reasoning (IJCAR'06, vol.4130, pp.281-286, 2006. ,
Interprocedural Shape Analysis with Separated Heap Abstractions, Proc. of the 13th International Static Analysis Symposium (SAS'06, vol.4134, pp.240-260, 2006. ,
BI as an Assertion Language for Mutable Data Structures, Proc. of the 28th Symposium on Principles of Programming Languages (POPL'01), pp.14-26, 2001. ,
Constraint Logic Programming: A Survey, Journal of Logic Programming, vol.19, pp.503-581, 1994. ,
A Machine-Checked Model for a Java-Like Language, Virtual Machine, and Compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.28, pp.619-695, 2006. ,
Specification and Verification Challenges for Sequential Object-Oriented Programs, Formal Aspects of Computing, vol.19, pp.159-189, 2007. ,
The Size-Change Principle for Program Termination, Proc. of the 28th Symposium on Principles of Programming Languages (POPL'01), pp.81-92, 2001. ,
, Formal Translation of Bytecode into BoogiePL. Electric Notes on Theoretical Computer Science, vol.190, pp.35-50, 2007.
Modular Verification of Static Class Invariants, Proc. of the 18th European Conference on Object-Oriented Programming, vol.3086, pp.26-42, 2004. ,
Class-local Object Invariants, Proc. of the 1st India Software Engineering Conference (ISEC'08), 2008. ,
, The Java TM Virtual Machine Specification, 1999.
Model Checking Real Time Java using Java PathFinder, Proc. of the 3rd International Symposium on Automated Technology for Verification and Analysis, vol.3707, pp.444-456, 2005. ,
Refinement-Based Verification for Possibly-Cyclic Lists, Proc. of Theory and Practice of Program Analysis and Compilation, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, vol.4444, pp.247-272, 2006. ,
On the Relative Completeness of Bytecode Analysis versus Source Code Analysis, Proc. of the 17th International Conference on Compiler Construction (CC'08, pp.197-212, 2008. ,
Integrating Static Analysis and General-Purpose Theorem Proving for Termination Analysis, Proc. of the 28th International Conference on Software Engineering (ICSE'06, pp.873-876, 2006. ,
Termination Analysis with Calling Context Graphs, Proc. of the 18th International Conference on Computer Aided Verification (CAV'06, vol.4144, pp.401-414, 2006. ,
Core Semantics of Multithreaded Java, Proc. of the ACM Java Grande Conference, pp.29-38, 2001. ,
The Java Memory Model, Proc. of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05, pp.378-391, 2005. ,
Inferring Left-terminating Classes of Queries for Constraint Logic Programs, Proceedings of the 1996 Joint Int. Conference and Symposium on Logic Programming, pp.7-21, 1996. ,
cTI: a constraint-based Termination Inference tool for ISO-Prolog, Theory and Practice of Logic Programming, vol.5, pp.243-257, 2005. ,
Recurrence with Affine Level Mappings is P-time Decidable for CLP(R), Theory and Practice of Logic Programming, vol.8, pp.111-119, 2008. ,
The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19, vol.1, pp.31-100, 2006. ,
The Pitfalls of Verifying Floating-Point Computations, Proc. of the Workshop on Verified Software: Theories, Tools, Experiments (VSTTE'07, vol.30, 2007. ,
Object-Oriented Type Inference, Proc. of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'91, vol.26, pp.146-161, 1991. ,
Magic-Sets Transformation for the Analysis of Java Bytecode, Proc. of the 14th International Static Analysis Symposium (SAS'07), vol.4634, pp.452-467, 2007. ,
Pure Versus Impure Lisp, ACM Transactions on Programming Languages and Systems, vol.19, pp.223-238, 1997. ,
Termination Proofs for Logic Programs, Lecture Notes in Computer Science, vol.446, 1990. ,
A Complete Method for Synthesis of Linear Ranking Functions, Proc. of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04, vol.2937, pp.239-251, 2004. ,
Transition Invariants, Proc. of the 19th IEEE Symposium on Logic in Computer Science (LICS'04), pp.32-41, 2004. ,
Transition Predicate Abstraction and Fair Termination, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.29, p.3, 2007. ,
Distinctness and Sharing Domains for Static Analysis of Java Programs, Proc. of the 15th European Conference on Object-Oriented Programming (ECOOP'01), vol.2072, pp.77-98, 2001. ,
Intuitionistic Reasoning about Shared Mutable Data Structure, Proc. of Millennial Perspectives in Computer Science, Symposium in Honour of Sir Tony Hoare, pp.303-321, 2000. ,
Detecting Non-Cyclicity by Abstract Compilation into Boolean Functions, Proc. of the 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06, vol.3855, pp.95-110, 2006. ,
Purity and Side Effect Analysis for Java Programs, Proc. of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'05, vol.3385, pp.199-215, 2005. ,
Automated Termination Analysis for Logic Programs by Term Rewriting, Proc. of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06), vol.4407, pp.177-193, 2006. ,
Pair-Sharing Analysis of Object-Oriented Programs, Proc. of Static Analysis Symposium (SAS'05, vol.3672, pp.320-335, 2005. ,
On Termination of Logic Programs with Floating Point Computations, Proc. of the 9th International Symposium on Static Analysis (SAS'02, vol.2477, pp.151-164, 2002. ,
The JULIA Static Analyser, 2008. ,
Nullness Analysis in Boolean Form, Proc. of the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM'08), 2008. ,
Path-Length Analysis for Object-Oriented Programs, First International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-01915777
Class Analyses as Abstract Interpretations of Trace Semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.25, pp.578-630, 2003. ,
Using CLP Simplifications to Improve Java Bytecode Termination Analysis, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-01188704
Julia + BinTerm: An Automatic Termination Prover for Java Bytecode, 2008. ,
Points-to Analysis in Almost Linear Time, Proc. of the 23th ACM Symposium on Principles of Programming Languages (POPL'96), pp.32-41, 1996. ,
Convexity and Optimization in Finite Dimensions I, 1970. ,
jMoped: A Test Environment for Java Programs, Proc. of the 19th International Conference on Computer Aided Verification (CAV'07, vol.4590, pp.164-167, 2007. ,
jMoped: A Java Bytecode Checker Based on Moped, Proc. of the 11th International Conference on Tools and Algorithms for the Construction and, 2005. ,