[Club2] Einladung: Formally Verified Certification of the Simplex Algorithm - Mi 22. Jun. 2022 14:30 - 14:50 (MESZ) (club2 at in.tum.de)

[piller at in.tum.de]

Sie wurden zum folgenden Termin eingeladen.

Titel: Formally Verified Certification of the Simplex Algorithm
Speaker: Adem Rimpapa

Abstract: Simplex solvers can be used to efficiently determine whether a  
linear program is feasible or infeasible. Directly verifying practical,  
optimised simplex solvers is often difficult due to the complexity of their  
code. Certification of simplex results is an alternative
approach to direct verification which involves tracing the algebraic  
operations of the simplex solver to produce a certificate, a proof of  
feasibility or infeasibility of a particular linear program. Certificates  
are checked using a piece of code called the certificate checker, which  
needs to be formally verified. This thesis provides an implementation of a  
certificate checker, a certificate parser, and modifications to a simplex  
solver for the purpose of certificate generation. The certificate checker  
is implemented in the interactive theorem prover Isabelle/HOL, with the end  
goal being verification of
soundness and completeness of the certificate checker. The code was  
evaluated on two example datasets. The first dataset only produced  
certificates for feasible linear programs and were all checked as valid by  
the certificate checker. The second dataset produced certificates for  
infeasible linear programs, most of which were declared to be invalid by  
the certificate checker. The results of the second dataset still need to be  
examined, since they could potentially lead to the discovery of a mistake  
in one of the components of the code.
Wann: Mi 22. Jun. 2022 14:30 – 14:50 Mitteleuropäische Zeit - Berlin
Kalender: club2 at in.tum.de
Wer
     * piller at in.tum.de- Veranstalter
     * club2 at in.tum.de
     * brandtf at in.tum.de
     * liedtke at ma.tum.de
     * mitja.krebs at tum.de
     * r.dardjonova at gmail.com
     * madlener at in.tum.de
     * sextl at in.tum.de
     * rimpapa at in.tum.de

Termininformationen:  
https://calendar.google.com/calendar/event?action=VIEW&eid=MGZmbGQzazE1Zjg1MGppZnFvY2lmOHRwcXMgY2x1YjJAaW4udHVtLmRl&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWM1YzkzODZhODZlZjczMTIzZTczYzc4ZWU4NzNlYTVhYzVjNGM3NmM&ctz=Europe%2FBerlin&hl=de&es=0

Einladung von Google Kalender: https://calendar.google.com/calendar/

Sie erhalten diese E-Mail unter club2 at in.tum.de, da Sie ein Gast bei diesem  
Termin sind.

Lehnen Sie diesen Termin ab, um keine weiteren Informationen zu diesem  
Termin zu erhalten. Sie können auch unter  
https://calendar.google.com/calendar/ ein Google-Konto erstellen und Ihre  
Benachrichtigungseinstellungen für Ihren gesamten Kalender steuern.

Wenn Sie diese Einladung weiterleiten, kann jeder Empfänger eine Antwort an  
den Organisator senden und zur Gästeliste hinzugefügt werden. Außerdem  
könnte er weitere Nutzer einladen und Ihre Antwort ändern. Weitere  
Informationen: https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20220620/e5049a2a/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 3791 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20220620/e5049a2a/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 3857 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20220620/e5049a2a/attachment-0001.bin>