• Pegasus: A Framework for Sound Continuous Invariant Generation

  

  cmu.edu

  Abstract: “Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to automation of formal proofs of safety in hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.”

          Comments
  

  formalmethods pdf programming

  • Add  

  1

More like this (3)

• Making Whiley Boogie! (2017)

  

  vuw.ac.nz

  Abstract: “The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#,...

  Abstract: “The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC/Java, SPARK Ada, and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a similar way to type checking. A common integration approach is to generate verification conditions that are handed off to an automated theorem prover. This provides a nice separation of concerns,...

  • Add  

  
• 

  TLA+ model checking made symbolic

  

  acolyer.org

  TLA+ model checking made symbolic Konnov et al., OOPSLA’19 TLA+ is a formal specification language (Temporal...

  TLA+ model checking made symbolic Konnov et al., OOPSLA’19 TLA+ is a formal specification language (Temporal Logic of Actions) particularly well suited to reasoning about distributed algorithms. In addition to the specification language, the TLA+ toolset includes a model checker (TLC) and a theorem prover (TLAPS). Given the huge state spaces involved in many real-world … Continue reading TLA+ model checking made symbolic

  • Read
  • Add  

  
• Automatic Loop Invariant Generation and Refinement through Selective Sampling (2017)

  

  lijiaying.github.io

  Abstract: “Automatic loop-invariant generation is important in program analysis and verification. In this work, we propose...

  Abstract: “Automatic loop-invariant generation is important in program analysis and verification. In this work, we propose a technique for automatic loop-invariant generation through a combination of active learning and verification. Given a Hoare triple of a program containing a loop, we start with randomly testing the program, collect program states at run-time and categorize them based on whether they satisfy the invariant to be...

  • Add  

  1