Programming Languages and Systems

DOI10.1007/B107380MaRDI QIDQ5316581zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia Cousot, Jerome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival

Publication date 13 September 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107380

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• Why does Astrée scale up?
• Programming Languages and Systems
• scientific article; zbMATH DE number 1953274
• Static Analysis
• Certified Static Analysis by Abstract Interpretation

Cited in

(49)

• PAG -- an efficient program analyzer generator
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• TASS: the toolkit for accurate scientific software
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• Formal analysis of the compact position reporting algorithm
• A decision tree lifted domain for analyzing program families with numerical features
• Testing your (static analysis) truths
• Fast and efficient bit-level precision tuning
• Verified functional programming of an abstract interpreter
• Multilevel static analysis for improving program quality
• Verified compilation of floating-point computations
• An approximation framework for solvers and decision procedures
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• A genetically modified Hoare logic
• Abstract interpretation of microcontroller code: intervals meet congruences
• Weakening additivity in adjoining closures
• ASTREE
• Static analysis of run-time errors in embedded critical parallel C programs
• Hardware-Dependent Proofs of Numerical Programs
• Splitting the Control Flow with Boolean Flags
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• A scalable segmented decision tree abstract domain
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Polynomial Precise Interval Analysis Revisited
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• Polynomial function intervals for floating-point software verification
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• An accurate join for zonotopes, preserving affine input/output relations
• Structural Abstract Interpretation: A Formal Study Using Coq
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Programming Languages and Systems
• Building certified static analysers by modular construction of well-founded lattices
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• A Hybrid Denotational Semantics for Hybrid Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Transfer function synthesis without quantifier elimination
• Static Analysis
• Semantic foundations for cost analysis of pipeline-optimized programs
• Source code analysis with a temporal extension of first-order logic
• Parallel program analysis via range splitting
• Adversarial reachability for program-level security analysis
• Context-sensitive meta-constraint systems for explainable program analysis
• Cone-based abstract interpretation for nonlinear positive invariant synthesis
• Poles-based invariant generation for verifying the BIBO stability of digital filters
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Why does Astrée scale up?
• Proof-carrying code from certified abstract interpretation and fixpoint compression

This page was built for publication: Programming Languages and Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5316581)