SMT-based model checking for recursive programs (Q518396): Difference between revisions

From MaRDI portal
Changed an Item
Normalize DOI.
 
(13 intermediate revisions by 6 users not shown)
Property / DOI
 
Property / DOI: 10.1007/s10703-016-0249-4 / rank
Normal rank
 
Property / describes a project that uses
 
Property / describes a project that uses: SMTInterpol / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Boogie / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: SPIN / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Bebop / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: CBMC / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: z3 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Spacer / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: UFO / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2571456046 / rank
 
Normal rank
Property / arXiv ID
 
Property / arXiv ID: 1405.4028 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2753756 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Tools and Algorithms for the Construction and Analysis of Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: From Under-Approximations to Over-Approximations and Back / rank
 
Normal rank
Property / cites work
 
Property / cites work: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems / rank
 
Normal rank
Property / cites work
 
Property / cites work: Precise interprocedural dataflow analysis with applications to constant propagation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Program invariants as fixedpoints / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3922128 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2754086 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2754081 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification / rank
 
Normal rank
Property / cites work
 
Property / cites work: Generalized Property Directed Reachability / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nested interpolants / rank
 
Normal rank
Property / cites work
 
Property / cites work: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: SAT-Based Model Checking without Unrolling / rank
 
Normal rank
Property / cites work
 
Property / cites work: Applying Linear Quantifier Elimination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5674430 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Solving SAT and SAT Modulo Theories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Linear quantifier elimination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lazy abstraction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Compositional may-must program analysis / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4417909 / rank
 
Normal rank
Property / DOI
 
Property / DOI: 10.1007/S10703-016-0249-4 / rank
 
Normal rank

Latest revision as of 20:08, 9 December 2024

scientific article
Language Label Description Also known as
English
SMT-based model checking for recursive programs
scientific article

    Statements

    SMT-based model checking for recursive programs (English)
    0 references
    0 references
    0 references
    0 references
    28 March 2017
    0 references
    model checking
    0 references
    may-must
    0 references
    satisfiability
    0 references
    quantifier elimination
    0 references
    recursion
    0 references
    compositional
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers