Analysis and Transformation of Constrained Horn Clauses for Program Verification (Q6063893): Difference between revisions

@@ Property / cites work @@
+Probabilistic Horn Clause Verification
@@ Property / cites work: Probabilistic Horn Clause Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Closed-form upper bounds in static cost analysis
@@ Property / cites work: Closed-form upper bounds in static cost analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Cost analysis of object-oriented bytecode programs
+Normal rank
@@ Property / cites work @@
+Test Case Generation of Actor Systems
@@ Property / cites work: Test Case Generation of Actor Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures for flat array properties
@@ Property / cites work: Decision procedures for flat array properties / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385536
@@ Property / cites work: Q4385536 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic programming and negation: A survey
@@ Property / cites work: Logic programming and negation: A survey / rank @@
+Normal rank
@@ Property / cites work @@
+Analysis of Linear Hybrid Systems in CLP
@@ Property / cites work: Analysis of Linear Hybrid Systems in CLP / rank @@
+Normal rank
@@ Property / cites work @@
+A bottom-up polymorphic type inference in logic programming
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Simple relational correctness proofs for static analyses and program transformations
+Normal rank
@@ Property / cites work @@
+Horn Clause Solvers for Program Verification
@@ Property / cites work: Horn Clause Solvers for Program Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanized semantics for the clight subset of the C language
+Normal rank
@@ Property / cites work @@
+SAT modulo linear arithmetic for solving polynomial constraints
+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 @@
+Q5310200
@@ Property / cites work: Q5310200 / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding floating-point logic with abstract conflict driven clause learning
+Normal rank
@@ Property / cites work @@
+Grammar-related transformations of logic programs
@@ Property / cites work: Grammar-related transformations of logic programs / rank @@
+Normal rank
@@ Property / cites work @@
+Polyvariant mixed computation for analyzer programs
+Normal rank
@@ Property / cites work @@
+Q2751365
@@ Property / cites work: Q2751365 / rank @@
+Normal rank
@@ Property / cites work @@
+A Transformation System for Developing Recursive Programs
+Normal rank
@@ Property / cites work @@
+An Integrated Approach to Assertion-Based Random Testing in Prolog
+Normal rank
@@ Property / cites work @@
+ICE-based refinement type discovery for higher-order functional programs
+Normal rank
@@ Property / cites work @@
+Relational cost analysis
@@ Property / cites work: Relational cost analysis / rank @@
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Q5227061
@@ Property / cites work: Q5227061 / rank @@
+Normal rank
@@ Property / cites work @@
+Exploiting goal independence in the analysis of logic programs
+Normal rank
@@ Property / cites work @@
+Bottom-up abstract interpretation of logic programs
+Normal rank
@@ Property / cites work @@
+Analyzing logic programs using “prop”-ositional logic programs and a magic wand
+Normal rank
@@ Property / cites work @@
+Q4281588
@@ Property / cites work: Q4281588 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract interpretation and application to logic programs
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+Q2767081
@@ Property / cites work: Q2767081 / rank @@
+Normal rank
@@ Property / cites work @@
+Semantics and Controllability of Time-Aware Business Processes*
+Normal rank
@@ Property / cites work @@
+Relational verification through Horn clause transformation
+Normal rank
@@ Property / cites work @@
+Predicate pairing with abstraction for relational verification
+Normal rank
@@ Property / cites work @@
+Predicate Pairing for program verification
@@ Property / cites work: Predicate Pairing for program verification / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Horn Clauses on Inductive Data Types Without Induction
+Normal rank
@@ Property / cites work @@
+Removing algebraic data types from constrained Horn clauses using difference predicates
+Normal rank
@@ Property / cites work @@
+Conjunctive partial deduction: foundations, control, algorithms, and experiments
+Normal rank
@@ Property / cites work @@
+Abstract interpretation of logic programs using magic transformations
+Normal rank
@@ Property / cites work @@
+Constraint-based deductive model checking
@@ Property / cites work: Constraint-based deductive model checking / rank @@
+Normal rank
@@ Property / cites work @@
+Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
+Normal rank
@@ Property / cites work @@
+Q4052071
@@ Property / cites work: Q4052071 / rank @@
+Normal rank
@@ Property / cites work @@
+Newtonian program analysis
@@ Property / cites work: Newtonian program analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Transformations of CLP modules
@@ Property / cites work: Transformations of CLP modules / rank @@
+Normal rank
@@ Property / cites work @@
+Syntax-guided termination analysis
@@ Property / cites work: Syntax-guided termination analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Why3 — Where Programs Meet Provers
@@ Property / cites work: Why3 — Where Programs Meet Provers / rank @@
+Normal rank
@@ Property / cites work @@
+Controlling Polyvariance for Specialization-based Verification
+Normal rank
@@ Property / cites work @@
+Q4421875
@@ Property / cites work: Q4421875 / rank @@
+Normal rank
@@ Property / cites work @@
+Program Development in Computational Logic
@@ Property / cites work: Program Development in Computational Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Improving Reachability Analysis of Infinite State Systems by Specialization
+Normal rank
@@ Property / cites work @@
+Generalization strategies for the verification of infinite state systems
+Normal rank
@@ Property / cites work @@
+Proving Theorems by Program Transformation
@@ Property / cites work: Proving Theorems by Program Transformation / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient generation of test data structures using constraint logic programming and program transformation
+Normal rank
@@ Property / cites work @@
+Dynamic partial-order reduction for model checking software
+Normal rank
@@ Property / cites work @@
+A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
+Normal rank
@@ Property / cites work @@
+Theory and practice of constraint handling rules
@@ Property / cites work: Theory and practice of constraint handling rules / rank @@
+Normal rank
@@ Property / cites work @@
+Q5020649
@@ Property / cites work: Q5020649 / rank @@
+Normal rank
@@ Property / cites work @@
+Failure tabled constraint logic programming by interpolation
+Normal rank
@@ Property / cites work @@
+Horn clauses as an intermediate representation for program analysis and transformation
+Normal rank
@@ Property / cites work @@
+Incremental Analysis of Logic Programs with Assertions and Open Predicates
+Normal rank
@@ Property / cites work @@
+Inference rules for proving the equivalence of recursive procedures
+Normal rank
@@ Property / cites work @@
+Test case generation for object-oriented imperative languages in CLP
+Normal rank
@@ Property / cites work @@
+Coinductive Logic Programming and Its Applications
+Normal rank
@@ Property / cites work @@
+Refinement of Trace Abstraction
@@ Property / cites work: Refinement of Trace Abstraction / rank @@
+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 @@
+Q4702568
@@ Property / cites work: Q4702568 / rank @@
+Normal rank
@@ Property / cites work @@
+Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
+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 @@
+The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
+Normal rank
@@ Property / cites work @@
+TRACER: A Symbolic Execution Tool for Verification
+Normal rank
@@ Property / cites work @@
+Software model checking
@@ Property / cites work: Software model checking / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287559
@@ Property / cites work: Q5287559 / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
+Normal rank
@@ Property / cites work @@
+An iterative approach to precondition inference using constrained Horn clauses
+Normal rank
@@ Property / cites work @@
+Tree dimension in verification of constrained Horn clauses
+Normal rank
@@ Property / cites work @@
+Q3774923
@@ Property / cites work: Q3774923 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract interpretation based on Alexander Templates
+Normal rank
@@ Property / cites work @@
+On the implementation of the probabilistic logic programming language ProbLog
+Normal rank
@@ Property / cites work @@
+SMT-based model checking for recursive programs
@@ Property / cites work: SMT-based model checking for recursive programs / rank @@
+Normal rank
@@ Property / cites work @@
+Linear resolution with selection function
@@ Property / cites work: Linear resolution with selection function / rank @@
+Normal rank
@@ Property / cites work @@
+Logic program specialisation through partial  deduction: Control issues
+Normal rank
@@ Property / cites work @@
+Q2767047
@@ Property / cites work: Q2767047 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723916
@@ Property / cites work: Q2723916 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+An efficient SMT solver for string constraints
@@ Property / cites work: An efficient SMT solver for string constraints / rank @@
+Normal rank
@@ Property / cites work @@
+Q3992908
@@ Property / cites work: Q3992908 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial evaluation in logic programming
@@ Property / cites work: Partial evaluation in logic programming / rank @@
+Normal rank
@@ Property / cites work @@
+Interval-Based Resource Usage Verification: Formalization and Prototype
+Normal rank
@@ Property / cites work @@
+Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
+Normal rank
@@ Property / cites work @@
+A Transformational Approach to Parametric Accumulated-Cost Static Profiling
+Normal rank
@@ Property / cites work @@
+A general framework for static profiling of parametric resource usage
+Normal rank
@@ Property / cites work @@
+Decidable logics combining heap structures and data
+Normal rank
@@ Property / cites work @@
+Q5613949
@@ Property / cites work: Q5613949 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4229041
@@ Property / cites work: Q4229041 / rank @@
+Normal rank
@@ Property / cites work @@
+A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
+Normal rank
@@ Property / cites work @@
+Concolic Testing in CLP
@@ Property / cites work: Concolic Testing in CLP / rank @@
+Normal rank
@@ Property / cites work @@
+Q2722069
@@ Property / cites work: Q2722069 / rank @@
+Normal rank
@@ Property / cites work @@
+Synchronizing Constrained Horn Clauses
@@ Property / cites work: Synchronizing Constrained Horn Clauses / rank @@
+Normal rank
@@ Property / cites work @@
+Compile-time derivation of variable dependency using abstract interpretation
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Q4023828
@@ Property / cites work: Q4023828 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract interpretation: a kind of magic
@@ Property / cites work: Abstract interpretation: a kind of magic / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Removing Superfluous Versions in Polyvariant Specialization of Prolog Programs
+Normal rank
@@ Property / cites work @@
+Convex Hull Abstractions in Specialization of CLP Programs
+Normal rank
@@ Property / cites work @@
+Transformation of logic programs: Foundations and techniques
+Normal rank
@@ Property / cites work @@
+The loop absorption and the generalization strategies for the development of logic programs and partial deduction
+Normal rank
@@ Property / cites work @@
+Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
+Normal rank
@@ Property / cites work @@
+Abstract Interpretation with Specialized Definitions
+Normal rank
@@ Property / cites work @@
+Q2723933
@@ Property / cites work: Q2723933 / rank @@
+Normal rank
@@ Property / cites work @@
+Optimized algorithms for incremental analysis of logic programs
+Normal rank
@@ Property / cites work @@
+Abstract multiple specialization and its application to program parallelization
+Normal rank
@@ Property / cites work @@
+Precise interprocedural dataflow analysis with applications to constant propagation
+Normal rank
@@ Property / cites work @@
+Induction for SMT Solvers
@@ Property / cites work: Induction for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+The Alexander Method - a technique for the processing of recursive axioms in deductive databases
+Normal rank
@@ Property / cites work @@
+An overview of the K semantic framework
@@ Property / cites work: An overview of the K semantic framework / rank @@
+Normal rank
@@ Property / cites work @@
+BEYOND TAMAKI-SATO STYLE UNFOLD/FOLD TRANSFORMATIONS FOR NORMAL LOGIC PROGRAMS
+Normal rank
@@ Property / cites work @@
+Q4518894
@@ Property / cites work: Q4518894 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5020662
@@ Property / cites work: Q5020662 / rank @@
+Normal rank
@@ Property / cites work @@
+Mixtus: An automatic partial evaluator for full Prolog
+Normal rank
@@ Property / cites work @@
+Q4221106
@@ Property / cites work: Q4221106 / rank @@
+Normal rank
@@ Property / cites work @@
+Unfold/fold transformation of stratified programs
@@ Property / cites work: Unfold/fold transformation of stratified programs / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Properties of Co-Logic Programs by Unfold/Fold Transformations
+Normal rank
@@ Property / cites work @@
+Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
+Normal rank
@@ Property / cites work @@
+Q5537599
@@ Property / cites work: Q5537599 / rank @@
+Normal rank
@@ Property / cites work @@
+Horn clause computability
@@ Property / cites work: Horn clause computability / rank @@
+Normal rank
@@ Property / cites work @@
+A lattice-theoretical fixpoint theorem and its applications
+Normal rank
@@ Property / cites work @@
+Automating induction for solving Horn clauses
@@ Property / cites work: Automating induction for solving Horn clauses / rank @@
+Normal rank
@@ Property / cites work @@
+Deforestation: Transforming programs to eliminate trees
+Normal rank
@@ Property / cites work @@
+On certain axiomatizations of arithmetic of natural and integer numbers
+Normal rank
@@ Property / cites work @@
+Q5016382
@@ Property / cites work: Q5016382 / rank @@
+Normal rank