Grammar Analysis and Parsing by Abstract Interpretation

DOI10.1007/978-3-540-71322-7_9zbMath1149.68389MaRDI 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

68Q45: Formal languages and automata

68Q55: Semantics in the theory of computing

68Q42: Grammars and rewriting systems

Related Items

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