BmoreDaniel

How to do induction on the real numbers

Posted by BmoreDaniel on Thursday February 25, 2016 @11:20AM
from the ucsd-pl.github.io dept.

http://ucsd-pl.github.io/veridrone/induction/2016/02/17/real-induction.html

Re:Drone horror stories involve new pilots; how can the community fix ... on Saturday October 31, 2015 @03:09PM (#10483731)

Education of beginner pilots is definitely important, but I think the author makes a mistake in dismissing the potential of new safety software (e.g. prevent drones from flying in dangerous places), especially if it is formally verified (e.g. veridrone.ucsd.edu).

Re:VeriDrone project: building quadcopters people can bet their lives ... on Thursday October 22, 2015 @07:13PM (#10435805)

I work on the VeriDrone project. We did not receive any funding from the HACMS project, but we have begun working with some folks from the SMACCMPilot project (http://smaccmpilot.org/index.html) that was funded by HACMS. We hope to eventually integrate with their platform in order to benefit from the guarantees they provide such as memory safety.

VeriDrone project: building quadcopters people can bet their lives on [video]

Posted by BmoreDaniel on Thursday October 22, 2015 @01:47PM
from the ucsd-pl.github.io dept.

http://ucsd-pl.github.io/veridrone/talk/2015/10/22/intro-cns-review.html#read-more

( Read More... | 4 comments | 21 points | on HN )

Re:Ask HN: The purest skills needed to become a programmer? on Monday January 26, 2015 @03:16AM (#8945998)

The most important skill for a programmer is to learn to think before you code: http://www.wired.com/2013/01/code-bugs-programming-why-we-ne....

Re:Investigating Higher Quality Software on Friday January 16, 2015 @04:23AM (#8897912)

Formal verification can prove the absence of bugs.

Re:How Microsoft dragged its development practices into the 21st century on Wednesday August 06, 2014 @02:10AM (#8141252)

The fact that specification and documentation are abandoned is pretty sad. Software should be adequately specified and specs should be kept up to date with code. Code is not a spec.

Re:Automating Formal Proofs for Reactive Systems on Monday June 23, 2014 @09:06AM (#7931684)

1) The code that users write in Reflex is the code that actually runs. This means that any guarantee about a Reflex program is a guarantee about the real life implementation of that program.

2) Reflex does not use testing to verify a user's code. Instead, Reflex automatically produces fully machine checkable proofs that user-provided code satisfies user-provided specifications. Machine checkable proofs (in a proof assistant) provide the strongest possible guarantee about one's code.