Verifying Whiley programs with Boogie (Q2102933): Difference between revisions

@@ Property / cites work @@
+Verification of Concurrent Systems with VerCors
@@ Property / cites work: Verification of Concurrent Systems with VerCors / rank @@
+Normal rank
@@ Property / cites work @@
+Program Logics for Certified Compilers
@@ Property / cites work: Program Logics for Certified Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Intersection and union types
@@ Property / cites work: Intersection and union types / rank @@
+Normal rank
@@ Property / cites work @@
+Q4343983
@@ Property / cites work: Q4343983 / rank @@
+Normal rank
@@ Property / cites work @@
+The vectorization of ITPACK 2C
@@ Property / cites work: The vectorization of ITPACK 2C / rank @@
+Normal rank
@@ Property / cites work @@
+Towards verifying nonlinear integer arithmetic
@@ Property / cites work: Towards verifying nonlinear integer arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q2721096
@@ Property / cites work: Q2721096 / rank @@
+Normal rank
@@ Property / cites work @@
+Using First-Order Theorem Provers in the Jahob Data Structure Verification System
+Normal rank
@@ Property / cites work @@
+Q4808834
@@ Property / cites work: Q4808834 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3046739
@@ Property / cites work: Q3046739 / rank @@
+Normal rank
@@ Property / cites work @@
+Experimenting on solving nonlinear integer arithmetic with incremental linearization
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Guarded commands, nondeterminacy and formal derivation of programs
+Normal rank
@@ Property / cites work @@
+Why3 — Where Programs Meet Provers
@@ Property / cites work: Why3 — Where Programs Meet Provers / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+The Multiple Assignment Statement
@@ Property / cites work: The Multiple Assignment Statement / rank @@
+Normal rank
@@ Property / cites work @@
+Q3925859
@@ Property / cites work: Q3925859 / rank @@
+Normal rank
@@ Property / cites work @@
+Typing Local Control and State Using Flow Analysis
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4417801
@@ Property / cites work: Q4417801 / rank @@
+Normal rank
@@ Property / cites work @@
+Solving Nonlinear Integer Arithmetic with MCSAT
@@ Property / cites work: Solving Nonlinear Integer Arithmetic with MCSAT / rank @@
+Normal rank
@@ Property / cites work @@
+The dynamic frames theory
@@ Property / cites work: The dynamic frames theory / rank @@
+Normal rank
@@ Property / cites work @@
+A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
+Normal rank
@@ Property / cites work @@
+How the design of JML accommodates both runtime assertion checking and formal verification
+Normal rank
@@ Property / cites work @@
+Efficient weakest preconditions
@@ Property / cites work: Efficient weakest preconditions / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Automating Induction with an SMT Solver
@@ Property / cites work: Automating Induction with an SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+A Polymorphic Intermediate Verification Language: Design and Logical Encoding
+Normal rank
@@ Property / cites work @@
+Q5447372
@@ Property / cites work: Q5447372 / rank @@
+Normal rank
@@ Property / cites work @@
+Stepwise refinement of heap-manipulating code in Chalice
+Normal rank
@@ Property / cites work @@
+RustHorn: CHC-Based Verification for Rust Programs
+Normal rank
@@ Property / cites work @@
+Building High Integrity Applications with SPARK
@@ Property / cites work: Building High Integrity Applications with SPARK / rank @@
+Normal rank
@@ Property / cites work @@
+Viper: A Verification Infrastructure for Permission-Based Reasoning
+Normal rank
@@ Property / cites work @@
+Fast Decision Procedures Based on Congruence Closure
+Normal rank
@@ Property / cites work @@
+Fast congruence closure and extensions
@@ Property / cites work: Fast congruence closure and extensions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+The Relationship between Separation Logic and Implicit Dynamic Frames
+Normal rank
@@ Property / cites work @@
+Sound and Complete Flow Typing with Unions, Intersections and Negations
+Normal rank
@@ Property / cites work @@
+Counterexample-guided quantifier instantiation for synthesis in SMT
+Normal rank
@@ Property / cites work @@
+Quantifier Instantiation Techniques for Finite Model Finding in SMT
+Normal rank
@@ Property / cites work @@
+Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
+Normal rank
@@ Property / cites work @@
+Q4808804
@@ Property / cites work: Q4808804 / rank @@
+Normal rank
@@ Property / cites work @@
+Logical types for untyped languages
@@ Property / cites work: Logical types for untyped languages / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Whiley programs with Boogie
@@ Property / cites work: Verifying Whiley programs with Boogie / rank @@
+Normal rank
@@ Property / cites work @@
+JMLUnit: The Next Generation
@@ Property / cites work: JMLUnit: The Next Generation / rank @@
+Normal rank