Project Everest

2017年9月13日

Traditionally, software is produced in this way: write some code, maybe do some code review, run unit-tests, and then hope it is correct. Hard experience shows that it is very hard for programmers to write bug-free software. These bugs are…

2017年6月2日

At any point in time on any day of the week, Microsoft’s cloud computing operations are under attack: The company detects a whopping 1.5 million attempts a day to compromise its systems. Microsoft isn’t just fending off those attacks. It’s…

2016年9月30日

The work we do these days on F* is often in service of Project Everest. The goal of Everest is to verify and deploy a drop-in replacement for the HTTPS stack, the protocol using which you are probably reading this…

2016年9月20日

In the summer of 2015 a team of hackers attempted to take control of an unmanned military helicopter known as Little Bird. The helicopter, which is similar to the piloted version long-favored for U.S. special operations missions, was stationed at…

2016年7月21日

Samin Ishtiaq will be receiving the 2016 CAV Award for the development of Separation Logic and for demonstrating its applicability in the automated verification of programs that mutate data structures. He is winning this award alongside Josh Berdine, a former…