Horn Clause Solvers for Program Verification (Q2947164): Difference between revisions

@@ Property / describes a project that uses @@
+ESC/Java
@@ Property / describes a project that uses: ESC/Java / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HMC
@@ Property / describes a project that uses: HMC / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-319-23534-9_2
+Normal rank
@@ Property / OpenAlex ID @@
+W2293809538
@@ Property / OpenAlex ID: W2293809538 / rank @@
+Normal rank
@@ Property / cites work @@
+Booster: An Acceleration-Based Verification Framework for Array Programs
+Normal rank
@@ Property / cites work @@
+Q4385536
@@ Property / cites work: Q4385536 / rank @@
+Normal rank
@@ Property / cites work @@
+Resourceful Reachability as HORN-LA
@@ Property / cites work: Resourceful Reachability as HORN-LA / rank @@
+Normal rank
@@ Property / cites work @@
+A constraint-based approach to solving games on infinite graphs
+Normal rank
@@ Property / cites work @@
+Property Directed Polyhedral Abstraction
@@ Property / cites work: Property Directed Polyhedral Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Q3791123
@@ Property / cites work: Q3791123 / rank @@
+Normal rank
@@ Property / cites work @@
+Inadequacy of computable loop invariants
@@ Property / cites work: Inadequacy of computable loop invariants / rank @@
+Normal rank
@@ Property / cites work @@
+SAT-Based Model Checking without Unrolling
@@ Property / cites work: SAT-Based Model Checking without Unrolling / rank @@
+Normal rank
@@ Property / cites work @@
+A Transformation System for Developing Recursive Programs
+Normal rank
@@ Property / cites work @@
+Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
+Normal rank
@@ Property / cites work @@
+Soundness and Completeness of an Axiom System for Program Verification
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+Some characterization theorems for infinitary universal Horn logic without equality
+Normal rank
@@ Property / cites work @@
+Q4144755
@@ Property / cites work: Q4144755 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition as a decision procedure for timed automata
+Normal rank
@@ Property / cites work @@
+Q5584402
@@ Property / cites work: Q5584402 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4997236
@@ Property / cites work: Q4997236 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about procedures as parameters in the language L4
+Normal rank
@@ Property / cites work @@
+Model Checking Recursive Programs with Exact Predicate Abstraction
+Normal rank
@@ Property / cites work @@
+An overview of Ciao and its design philosophy
@@ Property / cites work: An overview of Ciao and its design philosophy / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Generalized Property Directed Reachability
@@ Property / cites work: Generalized Property Directed Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+Accelerating Interpolants
@@ Property / cites work: Accelerating Interpolants / rank @@
+Normal rank
@@ Property / cites work @@
+On sentences which are true of direct unions of algebras
+Normal rank
@@ Property / cites work @@
+Q4391452
@@ Property / cites work: Q4391452 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287559
@@ Property / cites work: Q5287559 / rank @@
+Normal rank
@@ Property / cites work @@
+Property-directed inference of universal invariants or proving their absence
+Normal rank
@@ Property / cites work @@
+Efficient weakest preconditions
@@ Property / cites work: Efficient weakest preconditions / rank @@
+Normal rank
@@ Property / cites work @@
+Temporal Verification of Reactive Systems: Response
+Normal rank
@@ Property / cites work @@
+Complexity, convexity and combinations of theories
+Normal rank
@@ Property / cites work @@
+Separation Logic Modulo Theories
@@ Property / cites work: Separation Logic Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Synthesis and transformation of logic programs using unfold/fold proofs
+Normal rank
@@ Property / cites work @@
+Lower bounds for resolution and cutting plane proofs and monotone computations
+Normal rank
@@ Property / cites work @@
+A type-directed abstraction refinement approach to higher-order model checking
+Normal rank
@@ Property / cites work @@
+Precise interprocedural dataflow analysis with applications to constant propagation
+Normal rank
@@ Property / cites work @@
+Low-level liquid types
@@ Property / cites work: Low-level liquid types / rank @@
+Normal rank
@@ Property / cites work @@
+The concept of a supercompiler
@@ Property / cites work: The concept of a supercompiler / rank @@
+Normal rank
@@ Property / cites work @@
+The Semantics of Predicate Logic as a Programming Language
+Normal rank