Precondition Calculation for Loops Iterating over Data Structures

No abstract is available for this paper.

• Publication year

  2016

• Venue

  International Conference on Software Quality, Reliability and Security

• Publication date

  2016-08-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/QRS.2016.25
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Juggrnaut: using graph grammars for abstracting unbounded heap structures

  2015cited by this paper
• Assertion-Directed Precondition Synthesis for Loops over Data Structures

  2015cited by this paper
• Generating Abstract Graph-Based Procedure Summaries for Pointer Programs

  2014cited by this paper
• Feedback-driven dynamic invariant discovery

  2014cited by this paper
• Weakest Precondition Synthesis for Compiler Optimizations

  2014cited by this paper
• Post-condition-Directed Invariant Inference for Loops over Data Structures

  2014cited by this paper
• Counterexample-Guided Precondition Inference

  2013cited by this paper
• Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs

  2013cited by this paper
• Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures

  2013cited by this paper
• Invariants for finite instances and beyond

  2013cited by this paper
• Invariant assertions, invariant relations, and invariant functions

  2013cited by this paper
• Deciding Conditional Termination

  2012cited by this paper
• Loop Summarization and Termination Analysis

  2011cited by this paper
• Computing Preconditions and Postconditions of While Loops

  2011cited by this paper
• Efficient Directionless Weakest Preconditions

  2011cited by this paper
• Automatic partial loop summarization in dynamic test generation

  2011cited by this paper
• Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

  2009cited by this paper
• Sufficient Preconditions for Modular Assertion Checking

  2008cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Ranking Abstractions

  2008cited by this paper
• Proving Conditional Termination

  2008cited by this paper
• Invariant Synthesis for Combined Theories

  2007cited by this paper
• Efficient weakest preconditions

  2005cited by this paper
• Weakest-precondition of unstructured programs

  2005cited by this paper
• A framework for numeric analysis of array operations

  2005cited by this paper
• Verification of Java Programs Using Symbolic Execution and Invariant Generation

  2004cited by this paper
• Avoiding exponential explosion: generating compact verification conditions

  2001cited by this paper
• Guarded commands, nondeterminacy and formal derivation of programs

  1975cited by this paper

• C2S: translating natural language comments to formal program specifications

  2020cites this paper