Logic, Types, and Programs Meetup

Do 23.06.2016 (19:00 - 21:30 Uhr)

Logic types programs

The Logic, Types, and Programs Meetup aims to connect people who are interested in formal logic and its various applications, such as software verification, formal mathematics, type systems, or philosophy. We will not restrict ourself to one application, but instead try to explore and learn in an open ended fashion.

 

 

 

#3 – Real World Model Checking Using SAT Solvers

Formal logic often looks more like an arcane art than an useful tool. One reason for this might be an apparent lack of good learning tools. This, however, is not entirely true.

 

It’s time for our third Meetup! This time Adrien will give tell us how SAT solvers are used by Systerel to solve real world model checking problems:

Formally proving properties on a given system can be done a number of ways. In this session, we present how SAT solvers can be used to do model checking on real-world systems. We’ll show how the world „formal“ does not necessarily imply dealing with high level logic concepts, and how the combination of a high level language that we translate to boolean clauses before giving them to a SAT solver provides an effective and versatile proof tool.

Please sign in and get to know more about this event at meetup.com.

 


Veranstaltungsort

leanovate GmbH, Berlin
Blücherstr. 22, 10961 Berlin

Lade Karte ...
© by leanovate GmbH - Impressum