Logical approximation for program analysis

DOI10.1007/S10990-011-9071-2MaRDI QIDQ1929363zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Robert J. Simmons, Frank Pfenning

Publication date 8 January 2013

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://figshare.com/articles/journal_contribution/Logical_approximation_for_program_analysis/6607040

zbMATH Keywords

abstract interpretationlogical frameworksprogram analysisordered linear logicsubstructural operational semantics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Abstract interpretation and application to logic programs
• A proof-theoretic approach to the static analysis of logic programs
• Publication:3201751
• Bottom-up abstract interpretation of logic programs
• Logical Interpretation: Static Program Analysis Using Theorem Proving

Cites work

• scientific article; zbMATH DE number 2080051 (Why is no real title available?)
• scientific article; zbMATH DE number 1765675 (Why is no real title available?)
• scientific article; zbMATH DE number 2090529 (Why is no real title available?)
• scientific article; zbMATH DE number 1420794 (Why is no real title available?)
• scientific article; zbMATH DE number 5254145 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Abstract interpreters for free
• Abstracting abstract machines
• An effective fixpoint semantics for linear logic programs
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Flattening and saturation: Two representation changes for generalization
• Forum: A multiple-conclusion specification logic
• K-Maude: a rewriting based tool for semantics of programming languages
• Language in action. Categories, lambdas and dynamic logic
• Linear Logical Algorithms
• Linguistic application of first order intuitionistic linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Logic programming in a fragment of intuitionistic linear logic
• Logical approximation for program analysis
• Model checking linear logic specifications
• On the complexity analysis of static analyses
• Principles and implementation of deductive parsing
• Relating complexity and precision in control flow analysis
• Relating state-based and process-based concurrency through linear logic (full-version)
• The Mathematics of Sentence Structure
• The rewriting logic semantics project
• Types for Proofs and Programs
• Uniform proofs as a foundation for logic programming

Cited in

(11)

• Approximate bit dependency analysis to identify program synthesis problems as infeasible
• Logical approximation for program analysis
• Extracting program logics from abstract interpretations defined by logical relations
• scientific article; zbMATH DE number 2086611 (Why is no real title available?)
• Analogical logic program synthesis algorithm that can refute inappropriate similarities
• A proof-theoretic approach to the static analysis of logic programs
• scientific article; zbMATH DE number 781170 (Why is no real title available?)
• Lookahead analysis in exact real arithmetic with logical methods
• Structural focalization
• Analysis of Boolean Programs
• scientific article; zbMATH DE number 2012389 (Why is no real title available?)

Describes a project that uses

Uses Software

• K tool
• K-Maude
• K Prover
• Lolli

This page was built for publication: Logical approximation for program analysis

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