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. Conferences, Workshops, Symposiums, and Seminars
  4. -Overify: Optimizing Programs for Fast Verification
 
conference paper

-Overify: Optimizing Programs for Fast Verification

Wagner, Jonas  
•
Kuznetsov, Volodymyr  
•
Candea, George  
2013
14th Workshop on Hot Topics in Operating Systems (HotOS XIV)
14th Workshop on Hot Topics in Operating Systems (HotOS XIV)

Developers rely on automated testing and verification tools to gain confidence in their software. The input to such tools is often generated by compilers that have been designed to generate code that runs fast, not code that can be verified easily and quickly. This makes the verification tool's task unnecessarily hard. We propose that compilers support a new kind of switch, -Overify, that generates code optimized for the needs of verification tools. We implemented this idea for one class of verification (symbolic execution) and found that, when run on the Coreutils suite of UNIX utilities, it reduces verification time by up to 95x.

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

overify.pdf

Access type

openaccess

Size

517.08 KB

Format

Adobe PDF

Checksum (MD5)

8836a9ae65ecdcf3728a27c3c0186534

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