Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Student works
  4. Verification of Imperative Programs in Scala
 
Loading...
Thumbnail Image
master thesis

Verification of Imperative Programs in Scala

Blanc, Régis William  
2012

Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a mathematical proof of correctness of programs. In this thesis, we present a verification procedure for imperative programs. Our procedure reduces imperative programming to functional programming and uses a semi-decision procedure that can reason modulo recursive functions. As a complementary method, we propose an algorithm to generate test cases that attain a high coverage of the program statements or can force the execution of some very refined control paths. We have implemented these algorithms and have integrated them in the Leon verification system. Leon can be used to verify programs written in a proper subset of Scala.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

main.pdf

Access type

openaccess

Size

878.88 KB

Format

Adobe PDF

Checksum (MD5)

25da88bc76075138c00560c301472244

Loading...
Thumbnail Image
Name

thesis.pdf

Access type

openaccess

Size

887.62 KB

Format

Adobe PDF

Checksum (MD5)

611d387430a52875401134fec1d89542

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés