Softwareverificatie onder resource revocatie met multi-modale separation logica KU Leuven
Rigoureuze software verificatie in wiskundig onderbouwde programmalogica's maakt het mogelijk om sterk vertrouwen op te bouwen in de correctheid van softwaresystemen. Het verbinden van verificatieresultaten op verschillende abstractieniveaus blijft echter moeilijk, met name in praktische programmeertalen en systemen waar eigendomswissels van hulpbronnen niet goed uitlijnen met contextwissels tussen softwarecomponenten. Dit project stelt ...