On May 15, 4:59 pm, Nuhaa All Bakry <[email protected]> wrote: > never heard of proof assistant before, how is it different from those > testing tools??
This wikipedia entry, especially the section on the Pentium FDIV bug, provides additional background: http://en.wikipedia.org/wiki/Automated_theorem_proving We're now seeing a migration of these techniques from hardware to software, and my proposed talk will focus on the latter. -- Kim-Ee > > On 15 May 2010, at 16:00, Harisfazillah Jamel > > > > <[email protected]> wrote: > > Hi, > > > Look good in devlopers tracks. Have you submit to > > >http://conf.oss.my/cfp.html > > > Thanks. > > > On Sat, May 15, 2010 at 10:28 AM, <[email protected]> wrote: > >> Hi everyone, > > >> I just submitted a talk proposal for MOSC 2010 titled "No Bugs, No > >> Holes: > >> Can Proof Assistants Help Achieve Software Perfection?" > > >> I was wondering if the topic would be of any interest at MOSC so I > >> thought > >> of asking you guys for some feedback. > > >> The abstract goes: "No one wants bugs in their code, especially not > >> those > >> exploitable as security loopholes by malicious adversaries. One > >> promising > >> (and controversial) solution relies on automated mathematics to > >> logically > >> prove that code not only is free of bugs such as buffer overflows > >> but also > >> meets strict security and correctness specifications. This talk > >> overviews > >> the history, controversy, challenges, and success stories of open- > >> source > >> proof assistants such as Coq and Isabelle/HOL. " > > >> To be honest, open-source tools like Coq are obscure except to a > >> small group > >> of software developers (who generally don't carry such titles on > >> their > >> business cards anyway). It's even been argued that they /should/ > >> remain > >> obscure. > > >> I was thinking however, that one way we could carve a (lucrative!) > >> niche for > >> ourselves is by focusing on high-value-add opportunities such as the > >> provisioning of high-assurance systems. Roughly speaking, high- > >> assurance > >> means that if the system fails, someone dies. Such projects by > >> their very > >> nature require nothing short of generous financial backing. > > >> One way such systems are successfully engineered is via mechanized > >> formal logic as embodied by so-called proof assistants. > > >> Any comments/questions on the viability of this topic for MOSC? > > >> -- Kim-Ee > > >> -- > >> Join Open Source Developers Club Malaysiahttp://www.osdc.my/ > > >> Facebook Fan page > > >>http://www.facebook.com/group.php?gid=98685301577 > > >>http://www.facebook.com/OSDC.my > > >> You received this message because you are subscribed to the Google > > >> Groups "OSDC.my Mailing List" group. > >> To post to this group, send email to [email protected] > >> To unsubscribe from this group, send email to > >> [email protected] > >> For more options, visit this group at > >>http://groups.google.com/group/osdcmy-list?hl=en > > > -- > > My Facebook > >http://www.facebook.com/linuxmalaysia > > > My Blog > >http://blog.harisfazillah.info/ > > > My Network > >http://www.facebook.com/pages/Bukan-Sekadar-Internet-Sahaja/100866715422 > > >http://linuxdotmy.multiply.com/ > > > -- > > Join Open Source Developers Club Malaysiahttp://www.osdc.my/ > > > Facebook Fan page > > >http://www.facebook.com/group.php?gid=98685301577 > > >http://www.facebook.com/OSDC.my > > > You received this message because you are subscribed to the Google > > > Groups "OSDC.my Mailing List" group. > > To post to this group, send email to [email protected] > > To unsubscribe from this group, send email to > > [email protected] > > For more options, visit this group at > >http://groups.google.com/group/osdcmy-list?hl=en > > -- > Join Open Source Developers Club Malaysiahttp://www.osdc.my/ > > Facebook Fan page > > http://www.facebook.com/group.php?gid=98685301577 > > http://www.facebook.com/OSDC.my > > You received this message because you are subscribed to the Google > > Groups "OSDC.my Mailing List" group. > To post to this group, send email to [email protected] > To unsubscribe from this group, send email to > [email protected] > For more options, visit this group > athttp://groups.google.com/group/osdcmy-list?hl=en -- Join Open Source Developers Club Malaysia http://www.osdc.my/ Facebook Fan page http://www.facebook.com/group.php?gid=98685301577 http://www.facebook.com/OSDC.my You received this message because you are subscribed to the Google Groups "OSDC.my Mailing List" group. To post to this group, send email to [email protected] To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/osdcmy-list?hl=en
