Bohne
Subproject |
S2 |
Categories |
Systems of systems / blackbox tools |
Overview |
Bohne automatically verifies safety properties of infinite state systems whose behavior is expressed by (dynamically changing) graphs. |
T. Wies, Marco Muniz, and V. Kuncak. An efficient decision procedure for imperative tree data structures. In International Conference on Automated Deduction (CADE-23), Lecture Notes in Computer Science (LNCS), 2011. To appear. A. Podelski and T. Wies. Counterexample-guided focus. In Manuel V. Hermenegildo and Jens Palsberg, editors, 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 249-260, 2010. A. Podelski, A. Rybalchenko, and T. Wies. Heap assumptions on demand. In Aarti Gupta and Sharad Malik, editors, 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science (LNCS), pages 314-327, 2008. C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard. Using first-order theorem provers in the Jahob data structure verification system. In 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), volume 4349 of Lecture Notes in Computer Science (LNCS), pages 74-88, 2007. T. Wies, V. Kuncak, Karen Zee, A. Podelski, and M. Rinard. Verifying Complex Properties using Symbolic Shape Analysis. In Workshop on Heap Analysis and Verification (HAV), 2007. T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard. Field constraint analysis. In E. Allen Emerson and Kedar S. Namjoshi, editors, 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), volume 3855 of Lecture Notes in Computer Science (LNCS), pages 157-173, 2006. A. Podelski and T. Wies. Boolean heaps. In Chris Hankin and Igor Siveroni, editors, 12th International Static Analysis Symposium (SAS 2005), volume 3672 of Lecture Notes in Computer Science (LNCS), pages 268-283, 2005. |
|
Benchmarks |
--- |
Download |
|
Manual |
|
Status |
Prototype |