• Efficient verification of packet networks 

    Yang, Hongkun (2016-01-15)
    Network management will benefit from automated tools based upon formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying network properties in the data plane. This ...
  • Efficient, mechanically-verified validation of satisfiability solvers 

    Wetzler, Nathan David; 0000-0002-6174-923X (2015-05-06)
    Satisfiability (SAT) solvers are commonly used for a variety of applications, including hardware verification, software verification, theorem proving, debugging, and hard combinatorial problems. These applications rely on ...
  • Theory and techniques for synthesizing efficient breadth-first search algorithms 

    Nedunuri, Srinivas (2012-10-05)
    The development of efficient algorithms to solve a wide variety of combinatorial and planning problems is a significant achievement in computer science. Traditionally each algorithm is developed individually, based on ...
  • A verified framework for symbolic execution in the ACL2 theorem prover 

    Swords, Sol Otis (2011-02-11)
    Mechanized theorem proving is a promising means of formally establishing facts about complex systems. However, in applying theorem proving methodologies to industrial-scale hardware and software systems, a large amount ...
  • Weak-memory local reasoning 

    Wehrman, Ian Anthony (2012-11-20)
    Program logics are formal logics designed to facilitate specification and correctness reasoning for software programs. Separation logic, a recent program logic for C-like programs, has found great success in automated ...