| Date | Presenter | Paper |
|---|---|---|
| 04/18 | Jeff Potluck | Verifying parallel code after refactoring using equivalence checking by Abadi, Moria and Keidar-Barner, Sharon and Pidan, Dmitry and Veksler, Tatyana International Journal of Parallel Programming, 2019 @article{abadi2019verifying, title={Verifying parallel code after refactoring using equivalence checking}, author={Abadi, Moria and Keidar-Barner, Sharon and Pidan, Dmitry and Veksler, Tatyana}, journal={International Journal of Parallel Programming}, volume={47}, number={1}, pages={59--73}, year={2019}, publisher={Springer} } |
| Seth Laurenceau | Decidable Verification of Uninterpreted Programs by Umang Mathur, P. Madhusudan, and Mahesh Viswanathan POPL 2019 @article{10.1145/3290359, author = {Mathur, Umang and Madhusudan, P. and Viswanathan, Mahesh}, title = {Decidable Verification of Uninterpreted Programs}, year = {2019}, issue_date = {January 2019}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {3}, number = {POPL}, url = {https://doi.org/10.1145/3290359}, doi = {10.1145/3290359}, abstract = {We study the problem of completely automatically verifying uninterpreted programs—programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants, contracts, etc. being provided. We show that this problem is undecidable in general. The main contribution of this paper is a subclass of programs, called coherent programs that admits decidable verification, and can be decided in Pspace. We then extend this class of programs to classes of programs that are k-coherent, where k ∈ ℕ, obtained by (automatically) adding k ghost variables and assignments that make them coherent. We also extend the decidability result to programs with recursive function calls and prove several undecidability results that show why our restrictions to obtain decidability seem necessary.}, journal = {Proc. ACM Program. Lang.}, month = {jan}, articleno = {46}, numpages = {29}, keywords = {Decidability, Streaming Congruence Closure, Program Verification, Uninterpreted Programs, Coherence} } |
|
| Joseph Wolf | A Concept of
Software Shell for Interactive Mathematical Proof Verification Systems by Kleschev, Alexander S. and Moskalenko, Philip M. and Timchenko, Vadim A. Mathematical Modeling in Physics and Technology, 2019 @article{kleschev_moskalenko_timchenko_2019, title={A Concept of Software Shell for Interactive Mathematical Proof Verification Systems}, volume={2426}, journal={Mathematical Modeling in Physics and Technology}, author={Kleschev, Alexander S. and Moskalenko, Philip M. and Timchenko, Vadim A.}, year={2019}, month={Sep}, pages={153–160}} |
|
| 04/21 | Andrew Wilkerson | CPAchecker: A tool for configurable software verification by Beyer, Dirk and Keremoglu, M. Erkan Computer Aided Verification, 2011. Also, see: SV-COMP 2019 overview paper. @InProceedings{10.1007/978-3-642-22110-1_16, author="Beyer, Dirk and Keremoglu, M. Erkan", editor="Gopalakrishnan, Ganesh and Qadeer, Shaz", title="CPAchecker: A Tool for Configurable Software Verification", booktitle="Computer Aided Verification", year="2011", publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="184--190", abstract="Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, implements the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results --- we aim at accelerating this process. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this flexible and easy-to-extend platform, and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as eclipse plug-in. CPAchecker implements CPAs for several abstract domains. We evaluate the efficiency of the current version of our tool on software-verification benchmarks from the literature, and compare it with other state-of-the-art model checkers. CPAchecker is an open-source toolkit and publicly available.", isbn="978-3-642-22110-1" } |
| Alexandre Fernandez | HACLxN: Verified Generic SIMD Crypto by Polubelova, Marina and Bhargavan, Karthikeyan and Protzenko, Jonathan and Beurdouche, Benjamin and Fromherz, Aymeric and Kulatova, Natalia and Zanella-Béguelin, Santiago ACM Conference on Computer and Communications Security (CCS), 2020. @inproceedings{polubelova2020hacl, author = {Polubelova, Marina and Bhargavan, Karthikeyan and Protzenko, Jonathan and Beurdouche, Benjamin and Fromherz, Aymeric and Kulatova, Natalia and Zanella-Béguelin, Santiago}, title = {HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)}, organization = {ACM}, booktitle = {ACM Conference on Computer and Communications Security (CCS)}, year = {2020}, month = {November}, abstract = {We present a new methodology for building formally verified cryptographic libraries that are optimized for multiple architectures. In particular, we show how to write and verify generic crypto code in the F* programming language that exploits single-instruction multiple data (SIMD) parallelism. We show how this code can be compiled to platforms that support vector instructions, including ARM Neon and Intel AVX, AVX2, and AVX512. We apply our methodology to obtain verified vectorized implementations on all these platforms for the ChaCha20 encryption algorithm, the Poly1305 one-time MAC, and the SHA-2 and Blake2 families of hash algorithms. A distinctive feature of our approach is that we share code and verification effort between scalar and vectorized code, between vectorized code for different platforms, and between implementations of different cryptographic primitives. By doing so, we significantly reduce the manual effort needed to add new implementations to our verified library. In this paper, we describe our methodology and verification results, evaluate the performance of our code, and describe its integration into the HACL* cryptographic library. Our vectorized code has already been incorporated into several software projects, including the Firefox web browser.}, publisher = {ACM}, url = {https://www.microsoft.com/en-us/research/publication/haclxn/}, } |
|
| Misha Shiltsev | CREST: Hardware Formal Verification with ANSI-C Reference Specifications by Andreas Tiemeyer and Tom Melham and Daniel Kroening and John O'Leary. arXiv, 2019. @misc{tiemeyer2019crest, title={CREST: Hardware Formal Verification with ANSI-C Reference Specifications}, author={Andreas Tiemeyer and Tom Melham and Daniel Kroening and John O'Leary}, year={2019}, eprint={1908.01324}, archivePrefix={arXiv}, primaryClass={cs.PL} } |