C# Verification, Project ProposalDongliang XuC# Verification Program is designed to identify and validate applications developed using C# on .Net framework. The goal of this project is to survey and analyze the algorithms, methods and tools based on the software system being specified in C#. Meanwhile, I will try to write a prototype as an example to verify some related properties for simple application.In this project, I will try to concentrate on investigation into Spec# programming system which is a extension of the object-oriented language c#. I have used c# for both of academic courses and industry projects in past 5 years. This will be a great opportunity for me to deeply investigate into verification properties of the object-oriented language c#. First, I will survey related paper about Spec# and then summarize properties about the Spec# static program verifier, Boogie. Boogie, a unique component in Spec# uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it. Because my topic involves in verification for the special language, C#, I also will survey some paper about programming language and structure for C#. You may find them in the following reference list.Tools I will experiment with1. Boogie 2 (which supersedes BoogiePL) is a language for prescribing verification conditions.2. Spec# (pronounced "speck sharp") is a programming system aimed at improving the development and maintenance of correct software. It consists of the Spec# programming language (a superset of the object-oriented .NET language C#, adding non-null types and code contracts), the Spec# compiler (which emits run-time checks to enforce the contracts), and the Boogie static program verifier (which attempts to prove a program correct with respect to its contracts).Paper I will summarize( All of them are from Programming Languages and Methods group in Microsoft Research Redmond)1. Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter., The Spec# programming system: Challenges and directions. VSTTE 2005.2. Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. CASSIS 2004. 3. Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 2004. 4. K. Rustan M. Leino and Wolfram Schulte. Exception safety for C#. SEFM 2004. 5. Manuel Fähndrich and K. Rustan M. Leino. Declaring and checking non-null types in an object-oriented language. OOPSLA 2003.6. K. Rustan M. Leino and Peter Müller. Verification of equivalent-results methods. ESOP 2007. 7. K. Rustan M. Leino and Wolfram Schulte. Using history invariants to verify observers. ESOP 2007. 8. Ádám Darvas and K. Rustan M. Leino. Practical reasoning about invocations and implementations of pure methods. FASE 2007.9. K. Rustan M. Leino and Peter Müller. A verification methodology for model fields. ESOP 2006. 10. K. Rustan M. Leino and Peter Müller. Modular verification of static class invariants. FM 2005. 11. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO 2005. 12. Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff. HOL-Boogie -- an interactive prover for the Boogie program-verifier. To appear at TPHOLs 200813. K. Rustan M. Leino and Wolfram Schulte. A verifying compiler for a multi-threaded object-oriented language. To appear in the Marktoberdorf Summer School 2006 lecture notes. 14. Rob DeLine and K. Rustan M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70.15. Mike Barnett, Wolfram Schulte, and Nikolai Tillmann. .NET Contracts: Attaching Specifications to Components16. Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes. Model-Based Testing with AsmL.NET17. Mike Barnett and Wolfram Schulte. Runtime Verification of .NET Contracts18. P. Ferrara, F. Logozzo and M. Fähndrich. Safer unsafe code for .NET, in Proceedings of the 23rd ACM Conference on Object-oriented Programming (OOPSLA 2008). Nashville, TE, USA, October 19-23. ACM Press, New York, U.S.A.ScheduleI will read related paper in Oct.2008 and explore the usage for tools in Nov. Therefore, the progress report in the middle term will focus on theory and structure of Spec# and Boogie.Expected GoalTwo main goals should be achieved in the end of semester:1. I will give a related presentation to describe the architecture for Spec# and discuss important algorithms and strategies used in Spec#. Meanwhile, I will also display my case study(an example) about two tools: Boogie2 and Spec#. 2. I will write a survey report about this field, C# verification which should be in the fashion of a conference paper
View Full Document
Unlocking...