Programming Languages and Systems
From MaRDI portal
Publication:5316581
DOI10.1007/b107380zbMath1108.68422OpenAlexW4232919104MaRDI QIDQ5316581
Radhia Cousot, Antoine Miné, Patrick Cousot, Xavier Rival, Jerome Feret, Laurent Mauborgne, David Monniaux
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
Related Items
An approximation framework for solvers and decision procedures, ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness, Why does Astrée scale up?, Fast and efficient bit-level precision tuning, Verified functional programming of an abstract interpreter, Proof-carrying code from certified abstract interpretation and fixpoint compression, Wave equation numerical resolution: a comprehensive mechanized proof of a C program, System-level state equality detection for the formal dynamic verification of legacy distributed applications, A genetically modified Hoare logic, Semantic foundations for cost analysis of pipeline-optimized programs, 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, Splitting the Control Flow with Boolean Flags, Abstract interpretation of microcontroller code: intervals meet congruences, Polynomial function intervals for floating-point software verification, Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants, Formal analysis of the compact position reporting algorithm, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations, A Scalable Segmented Decision Tree Abstract Domain, Structural Abstract Interpretation: A Formal Study Using Coq, An Improved Tight Closure Algorithm for Integer Octagonal Constraints, Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions, A Hybrid Denotational Semantics for Hybrid Systems, Transfer Function Synthesis without Quantifier Elimination, A decision tree lifted domain for analyzing program families with numerical features, Weakening additivity in adjoining closures, ASTREE, Abstract Interpretation of Symbolic Execution with Explicit State Updates, Polynomial Precise Interval Analysis Revisited, Hardware-Dependent Proofs of Numerical Programs, Verified compilation of floating-point computations, Testing your (static analysis) truths
