Grammar Analysis and Parsing by Abstract Interpretation

DOI10.1007/978-3-540-71322-7_9zbMath1149.68389OpenAlexW2320520550MaRDI QIDQ3593074

Radhia Cousot, Patrick Cousot

Publication date: 24 September 2007

Published in: Program Analysis and Compilation, Theory and Practice (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71322-7_9

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42)

Related Items (77)

Differential Game Logic ⋮ Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ Automatic Inference of Access Permissions ⋮ Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Scalable polyhedral verification of recurrent neural networks ⋮ Compositional analysis for verification of parameterized systems ⋮ Gradual typing using union typing with records ⋮ Template-Based Unbounded Time Verification of Affine Hybrid Automata ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Static analysis of ReLU neural networks with tropical polyhedra ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Lightweight shape analysis based on physical types ⋮ Merge-and-Shrink Abstraction ⋮ Specialisation of Prolog and FCP programs using abstract interpretation ⋮ An integrated approach to high integrity software verification ⋮ Verifying constant-time implementations by abstract interpretation ⋮ A compiler framework for the reduction of worst-case execution times ⋮ On using data abstractions for model checking refinements ⋮ Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra ⋮ The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification ⋮ Lifting numeric relational domains to algebraic data types ⋮ Using Abstract Interpretation to Correct Synchronization Faults ⋮ An abstract interpretation framework for genotype elimination algorithms ⋮ Modeling of complex systems. II: A minimalist and unified semantics for heterogeneous integrated systems ⋮ Verification conditions for source-level imperative programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An abstract interpretation-based model for safety semantics ⋮ Improving Strategies via SMT Solving ⋮ Precise Interprocedural Analysis in the Presence of Pointers to the Stack ⋮ A sharing-based approach to supporting adaptation in service compositions ⋮ A two-phase approach for conditional floating-point verification ⋮ Analyzing infrastructure as code to prevent intra-update sniping vulnerabilities ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ Runtime abstract interpretation for numerical accuracy and robustness ⋮ Counterexample-Guided Refinement of Template Polyhedra ⋮ Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints ⋮ Refinement to certify abstract interpretations: illustrated on linearization for polyhedra ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ An array content static analysis based on non-contiguous partitions ⋮ From invariant checking to invariant inference using randomized search ⋮ Assume-admissible synthesis ⋮ Generic Abstraction of Dictionaries and Arrays ⋮ Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol ⋮ Formal Reduction for Rule-based Models ⋮ Loop invariants ⋮ Using abstract interpretation to add type checking for interfaces in Java bytecode verification ⋮ Automatic verification of parameterized networks of processes ⋮ Abstract interpretation of mobile systems ⋮ Pentagons: a weakly relational abstract domain for the efficient validation of array accesses ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ Demand-driven interprocedural analysis for map-based abstract domains ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes ⋮ Survey on Directed Model Checking ⋮ Static Analysis Techniques for Parameterised Boolean Equation Systems ⋮ Verifying Reference Counting Implementations ⋮ Program invariants as fixedpoints ⋮ Abstract interpretation and types for systems biology ⋮ Refinement-Based CFG Reconstruction from Unstructured Programs ⋮ Distributed and Predictable Software Model Checking ⋮ A decision tree lifted domain for analyzing program families with numerical features ⋮ A demonstrably correct compiler ⋮ Constructive Galois Connections ⋮ A Spectrum of Behavioral Relations over LTSs on Probability Distributions ⋮ A relational shape abstract domain ⋮ Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements ⋮ On the refinement of liveness properties of distributed systems ⋮ Abstract interpretation of resolution-based semantics ⋮ Interpreting Abstract Interpretations in Membership Equational Logic ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Automating the addition of fault tolerance with discrete controller synthesis ⋮ Mathematics for reasoning about loop functions ⋮ A sparse evaluation technique for detailed semantic analyses ⋮ Property-oriented expansion ⋮ Abstract cofibered domains: Application to the alias analysis of untyped programs

This page was built for publication: Grammar Analysis and Parsing by Abstract Interpretation