Web Formele correctheid

[Avi]

Ik ben al een tijdje op zoek naar bronmateriaal, werkteksten, thesissen, ..., over formele correctheid van programma's.
Op het internet vind ik niet zo fantastisch veel terug. Het lijkt ook vooral om een Europees concept te gaan tot zelfs iets wat hoofdzakelijk in de Benelux wordt onderwezen.

Wie nog oude cursusteksten of iets anders heeft liggen ik hoor het graag

 

[NoGo]

Als in formeel bewijzen dat een programma aan een bepaalde spec voldoet? Zelf enkel eens in aanraking gekomen op wat conferenties (over bvb. coq en afgeleiden), en eens gespeeld met JML maar had niet echt het gevoel dat het toen voor mij praktisch toepasbaar was. Meeste informatie wat ik me kan herinneren haalde ik ook maar uit hier en daar wat papers. Misschien dat er wat materiaal te vinden is voor een specifiek stuk software (zoals eerder genoemde?). Misschien kan je ook eens rondkijken op bijvoorbeeld c.stackexchange?

En anders ben ik wel benieuwd of iemand wat meer hier van heeft of weet te vinden

 

[Avi]

Als in formeel bewijzen dat een programma aan een bepaalde spec voldoet? Zelf enkel eens in aanraking gekomen op wat conferenties (over bvb. coq en afgeleiden), en eens gespeeld met JML maar had niet echt het gevoel dat het toen voor mij praktisch toepasbaar was. Meeste informatie wat ik me kan herinneren haalde ik ook maar uit hier en daar wat papers. Misschien dat er wat materiaal te vinden is voor een specifiek stuk software (zoals eerder genoemde?). Misschien kan je ook eens rondkijken op bijvoorbeeld c.stackexchange?

En anders ben ik wel benieuwd of iemand wat meer hier van heeft of weet te vinden

Formele correctheid wordt vooral academisch toegepast heb ik de indruk. Je gebruikt pre - en postcondities in combinatie met invarianten om een soort van ketting van waarheid aan elkaar te schakelen. Als je daar erin slaagt om de functionaliteit van een functie of klasse op die manier uit te drukken zou je formeel kunnen stellen dat hij correct is.

Het concept wordt nogal theoretisch omschreven in deze les gegeven door Dijkstra. Niet verbazend dat mensen met een zeer sterke wiskundige achtergrond ook grote aanhanger zijn van correctheid.

 

[NoGo]

Ja klopt, dat idee had ik ook. In ieder geval voor praktische toepassing, kan je dus software gebruiken om formeel proberen te bewijsen dat een stuk code aan een gegeven specificatie voldoet. Toen ik er zelf naar gekeken heb vond ik dat het veel te beperkt toepasbaar: een bak extra complexiteit om de spec te schrijven (waar ook fouten in kunnen zitten), algoritmes om het op te losse die niet efficient uitgevoerd kunnen worden, etc. Een degelijke test set is veel effectiever voor een groot deel van de software imo.

Misschien voor heel kritieke geconcentreerde stukjes code kan het wel nut hebben? IIRC gebruikten (gebruiken?) ze het bij NASA voor bepaalde systemen wel?

Straks eens de lecture bekijken, maar wel op 1.5x speed denk ik

 

[belloc]

Software foundations, Coq.
Zoek op programmeertalen zoals Agda en Lean theorem prover.

 

[CerumenCrevice]

Ik ben al een tijdje op zoek naar bronmateriaal, werkteksten, thesissen, ..., over formele correctheid van programma's.
Op het internet vind ik niet zo fantastisch veel terug. Het lijkt ook vooral om een Europees concept te gaan tot zelfs iets wat hoofdzakelijk in de Benelux wordt onderwezen.

Wie nog oude cursusteksten of iets anders heeft liggen ik hoor het graag

mijn master thesis ging over formele verificatie van zwakke geheugenconsistente systemen. Bij prof. Dr. Bart Jacobs aan de KULeuven, hij heeft een tool en heeft er heel wat over geschreven, dus misschien wel interessant: https://people.cs.kuleuven.be/~bart.jacobs/verifast/

 

[Avi]

n master thesis ging over formele verificatie van zwakke geheugenconsistente systemen. Bij prof. Dr. Bart Jacobs aan de KULeuven, hij heeft een tool en heeft er heel wat over geschreven, dus misschien wel interessant: https://people.cs.kuleuven.be/~bart.jacobs/verifast/

Super interessant! Ook les gehad van professor Jacobs dit jaar. Mag ik misschien een pdf van je thesis?

 

[CerumenCrevice]

Super interessant! Ook les gehad van professor Jacobs dit jaar. Mag ik misschien een pdf van je thesis?

Je kan er eens achter vragen bij KULeuven, maar eerlijk gezegd zou ik andere dingen erover lezen. Mijn thesis was nu niet meteen een meesterwerk te noemen en professor Jacobs heeft mij er ook maar net doorgelaten (terecht), dat kwam door omstandigheden toen.

Maar het topic is wel zeer interessant en professor Jacobs was zeer behulpzaam bij het promoten van de thesis, je kan hem altijd om extra leesvoer vragen. Vanuit een engineering standpunt is het leuk om te lezen wat er allemaal al gedaan is met formele verificatie en wat nog moeizaam verloopt etc.