Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Experiment Videos

Verifying OpenJDK's Sort Method for Generic Collections.

Stijn de Gouw1, Frank S de Boer2,3, Richard Bubel4

  • 12Studiecentrum Utrecht, Open University, Vondellaan 202, 3521 GZ Utrecht, Netherlands.

Journal of Automated Reasoning
|April 2, 2019
PubMed
Summary
This summary is machine-generated.

Related Concept Videos

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

Distributive laws for monotone specifications.

Acta informatica·2019
Same journal

Combining Higher-Order Logic with Set Theory Formalizations.

Journal of automated reasoning·2023
Same journal

Synthesising Programs with Non-trivial Constants.

Journal of automated reasoning·2023
Same journal

Unifying Splitting.

Journal of automated reasoning·2023
Same journal

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.

Journal of automated reasoning·2023
Same journal

A Formalization of SQL with Nulls.

Journal of automated reasoning·2022
Same journal

A Comprehensive Framework for Saturation Theorem Proving.

Journal of automated reasoning·2022
See all related articles

A bug in Java's TimSort algorithm, a widely used sorting method, was discovered during formal verification. This paper presents a corrected, exception-free version verified using the KeY tool, ensuring performance is maintained.

Area of Science:

  • Computer Science
  • Software Engineering

Background:

  • TimSort is a crucial sorting algorithm in Java and other frameworks.
  • Functional verification aims to ensure software correctness through formal methods.

Purpose of the Study:

  • To identify and fix a critical bug in the TimSort implementation.
  • To formally verify a new, bug-free version of TimSort.
  • To ensure the corrected algorithm maintains performance.

Main Methods:

  • Mechanical proofs using the KeY interactive verification tool.
  • Formal specification of the corrected TimSort version.
  • Analysis of proof complexity and required tool extensions.

Main Results:

  • Discovery of a bug causing uncaught exceptions in TimSort.
Keywords:
Case studyProgram verificationSpecificationTheorem proving

Related Experiment Videos

  • Development of a bug-free TimSort version.
  • Mechanical verification of termination and absence of exceptions for the new version.

    • Conclusions:

    • The verified bug-free TimSort version ensures stability without performance degradation.
    • The verification process highlighted the need for advanced capabilities in verification tools like KeY.