5 ms·
On the list of "cool things also happen to employ Z3", definitely check out MS Dafny programming language: https://github.com/Microsoft/dafny https://github.com
by Profan 8y ago
On the list of "cool things also happen to employ Z3", definitely check out MS Dafny programming language: https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny
- eggy 8y agoHow does Dafny differ from Microsoft's F* (FStar)[1]? [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
- pjmlp 8y agoIt is more C# like, and was used to write one of the Singularity post OSes at MS Research. "Automated Verification of a Type-Safe Operating System" https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/pldi117-yang.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
- eggy 8y agoThanks. I see the F#/F* synergy. Are C#/Dafny as similar to favor them over the F#/F* combo?
- lou1306 8y agoIvy [1] is another research language built around Z3. Slides from a recent presentation of the language are also available [2]. The concept of exploiting modularity to obtain decidable verification conditions is quite interesting. Plus, it compiles down to C++. [1]: http://microsoft.github.io/ivy/ http://microsoft.github.io/ivy/ [2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemon/wp/wordpress/wp-content/uploads/2019/01/winterschool19.pptx http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo... (PowerPoint slides)