(Hercule) Poirot is well known for his ability to solve difficult cases (aka concurrency bugs) that eluded the police (aka hard to find by conventional testing), often from within the confines of his home (aka statically without actually executing the program), using sharp logical reasoning (aka using theorem provers) with few mistakes (aka false alarms).
Try out Poirot live: http://www.rise4fun.com/Poirot
If you are using (or wish to use) Poirot in your research project, please drop us an email.
Poirot is a property checker for concurrent programs. It uses language-independent techniques to efficiently search the set of behaviors of a program for bugs. Consequently, Poirot can deal with programs written in a variety of languages. At this point, we plan to support C and .Net. Poirot4C (read Poirot-for-C) is available for download (see below). Poirot4.NET is coming soon.
Poirot works by first compiling the program in a supported language to a concurrent Boogie program. Next, it uses Corral, a symbolic exploration engine, to explore concurrent behaviors of the Boogie program looking for bugs. In case a bug is not found, Poirot produces a coverage report detailing the set of program behaviors that it covered.
Downloads
Download Poirot4C! Read here for notes on running Poirot4C.
Download Corral! Corral is a goal-directed symbolic exploration engine. It can be used as a stand-alone tool or in conjunction with other tools that use the Boogie language as their intermediate representation.
- Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012
- Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, no. MSR-TR-2012-9, January 2012
- Michael Emmi, Akash Lal, and Shaz Qadeer, Asynchronous programs with prioritized task buffers, no. MSR-TR-2012-1, January 2012
- Prathmesh Prabhu, Thomas Reps, Akash Lal, and Nicholas Kidd, Verifying Concurrent Programs via Bounded Context-Switching and Induction , November 2011
- Michael Emmi, Shaz Qadeer, and Zvonimir Rakamaric, Delay-bounded scheduling, in Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Association for Computing Machinery, Inc., January 2011
- Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009
- Akash Lal and Thomas Reps, Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis, in Formal Methods in System Design (FMSD), Springer Verlag, 2009
- K. Rustan M. Leino, This is Boogie 2, 24 June 2008
Poirot in Action
Sound and Unified Software Verification for Weak Memory Models. [website]
Getting Rid of Store-Buffers in the Analysis of Weak Memory Models. G. Parlato, F. Atig, A. Bouajjani. [paper, experiments]
How to Shop for Free Online – Security Analysis of Cashier-as-a-Service Based Web Stores. R. Wang, S. Chen, X. Wang, S. Qadeer. [paper]
