Re: [pl-seminar] Seminar this friday 3:30PM

[Julien Henry <jhenry@xxxxxxxxxxx>]

Hi all,

This Friday, I think I will talk about model-based decision procedures. State of the art SMT solvers are all based on the DPLL(T) framework, and use a SAT solver as a blackbox. This can be seen as an advantage, as advances on SAT directly transfer to performance improvements in SMT, but it is sometimes a drawback for e.g. conflict resolution. 

I will talk about a paper from De Moura and Jovanovic called âA Model-Constructing Satisfiability Calculusâ that describes a new approach called mcSAT. 

The paper can be found at http://csl.sri.com/users/dejan/papers/mcsat-vmcai2013.pdf

Thanks,

Julien

On Oct 1, 2015, at 5:01 PM, Tushar Sharma <tsharma@xxxxxxxxxxx> wrote:

Hi,

This friday, I will be talking about ICE framework. This is a framework to learn loop invariants with honesty and progress using black-box machine learning techniques. They build the framework for learning 1) numeric invariants, 2) heap invariants on arrays and lists. I will mostly focus on numeric invariants and we can have a brief discussion about heap invariants if time permit. The paper can be downloaded at:
http://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_5

Thanks,
Tushar

PS: I will not be baking or performing music. People close to me have revealed that it might be for the better :). If anyone else wants to volunteer, they can fill up this form:
https://docs.google.com/spreadsheets/d/1XO4sU5IXEra5QoWqMyW_Jzg9qi5fm4S3jPsRjIjwnDw/edit#gid=0

PPS: The slot for next week is empty. Take it quickly before it gets snatched up.

_______________________________________________
Pl-seminar mailing list
Pl-seminar@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar