2017 Spring
Welcome to the homepage of CSE645 (Spring 2017) Seminar in Languages!
General Information
Course description: We will read papers and discuss research ranging from high-level specifications (such as logic, rules, and sets) to algorithms and methods for efficient implementations, with applications in semantic web, program analysis, security, and services. If you are enrolled in the class, you must attend at least 50% of the meetings and to present a paper during the semester.
Instructors: Annie Liu, CR Ramakrishnan, Michael Kifer, David Warren, and Paul Fodor (contact: paul.fodor@stonybrook.edu).
Hours: Thursdays, 11:30AM-12:50PM, in New Computer Science Department room 220.
Schedule
1/26 Rustan Leino, Using Dafny to reason about concurrency, Microsoft
Dafny is a programming language and verification system primarily aimed at writing provably correct sequential programs. The expressivity of the Dafny language and the automation of its verifier also make Dafny suitable for more general reasoning tasks, along the lines of a general proof assistant. In this talk, I will present Dafny in its traditional setting. Then, I will use Dafny to model and prove correct the behavior of a concurrent algorithm. The style is inspired by UNITY, TLA+, and Event-B, to which Dafny adds automated reasoning.
SPEAKER’S BIO: Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. He is an ACM Fellow. Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he plays music and likes to cook.
Download: http://dafny.codeplex.com
Sources: https://github.com/Microsoft/dafny
2/2 Organizational meeting
2/9 Snow day.
2/16 Tiantian will present "Learning Executable Semantic Parsers for Natural Language Understanding". Percy Liang. Communications of ACM 2016.
http://cs.stanford.edu/~pliang/papers/executable-cacm2016.pdf
Answer Set Programming Introduction:
2/23 Paul will present a survey on ASP by Torsten Schaub (ICLP Autumn School 2016)
Slides: http://www.cs.uni-potsdam.de/~torsten/Potassco/Tutorials/iclp16.pdf
Manual: https://www.cs.utexas.edu/users/vl/teaching/378/guide-2.0.pdf
System: https://potassco.org
Run clingo online: http://potassco.sourceforge.net/clingo.html
ASP competition 2011: https://www.mat.unical.it/aspcomp2011/OfficialProblemSuite
DLV/DLVHex papers:
3/2 Taejun will present "The dlvhex system for knowledge representation: recent advances (system description)". Christoph Redl. TPLP 16(5-6): 866-883 (2016).
Paper: http://www.kr.tuwien.ac.at/staff/redl/publications/r2016-tplp.pdf
Slides: http://www.kr.tuwien.ac.at/staff/redl/publications/r2016-tplp-slides.pdf
Online system: http://www.kr.tuwien.ac.at/research/systems/dlvhex/demo.php
API: http://www.kr.tuwien.ac.at/research/systems/dlvhex/doc/group__pythonpluginframework.html
More advanced examples: http://www.kr.tuwien.ac.at/research/reports/rr1505.pdf
3/9 Feiyun will present "Combining Answer Set Programming and domain heuristics for solving hard industrial problems". Carmine Dodaro, Philip Gasteiger, Nicola Leone, Benjamin Musitsch, Francesco Ricca, Konstantin Schekotihin. TPLP 16(5-6): 653-669 (2016)
https://arxiv.org/pdf/1608.00730.pdf
Run DLV online: http://asptut.gibbi.com/
3/16 Spring break
Potassco papers:
3/23 Daniel will present "Modeling and Language Extensions". Martin Gebser, Torsten Schaub. AI Magazine 37(3): 33-44 (2016)
http://www.cs.uni-potsdam.de/wv/pdfformat/gebsch16a.pdf
Run clingo online: http://potassco.sourceforge.net/clingo.html
3/30 Ashkan will present "Clingo = ASP + Control: Preliminary Report". Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. arxiv 2014. (2014)
http://www.cs.uni-potsdam.de/wv/pdfformat/gekakasc14b.pdf
https://arxiv.org/pdf/1405.3694v1.pdf
Run clingo online: http://potassco.sourceforge.net/clingo.html
4/6 Chris will present "Ricochet Robots Reloaded. A Case-study in Multi-shot ASP Solving". Martin Gebser, Roland Kaminski, Philipp Obermeier, and Torsten Schaub. Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation 2015: 17-32 (2015)
http://www.cs.uni-potsdam.de/wv/pdfformat/gekaobsc15a.pdf
Run clingo online: http://potassco.sourceforge.net/clingo.html
Concurrency, IDP and probabilistic logic papers interleaved due to scheduling:
4/13 Shivanshu will present:
Communicating sequential processes. C. A. R. Hoare. CACM 1978.
http://dl.acm.org/citation.cfm?id=359585
and
Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis. Nicholas Ng, Nobuko Yoshida. CC 2016 Proceedings of the 25th International Conference on Compiler Construction.
https://www.doc.ic.ac.uk/~cn06/pub/2016/dingo/main.pdf
4/20 Tim Zhang will present "Open-World Probabilistic Databases". Ismail Ilkan Ceylan, Adnan Darwiche and Guy Van den Broeck. KR 2016.
http://web.cs.ucla.edu/~guyvdb/papers/CeylanKR16.pdf
4/27 Vasily will present "Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3." Maurice Bruynooghe, Hendrik Blockeel, Bart Bogaerts, Broes de Cat, Stef De Pooter, Joachim Jansen, Anthony Labarre, Jan Ramon, Marc Denecker, Sicco Verwer. TPLP 15(6): 783-817 (2015)
https://lirias.kuleuven.be/bitstream/123456789/448838/1/journal.pdf
Run IDP online: http://adams.cs.kuleuven.be/idp/server.html
5/4 Sarthak will present "A Logic-based Approach to Generatively Defined Discriminative Modeling" Taisuke Sato, Keiichi Kubota, Yoshitaka Kameya. ILP 2013 - 23rd International Conference on Inductive Logic Programming.
https://arxiv.org/abs/1410.3935
Stand discussions:
Papers
We will select papers from the following list (don't have to cover all) and possibly other interesting ones as they come up.
DLV/DLVHEX Interfaces between logic programming and imperative languages and Applications:
The dlvhex system for knowledge representation: recent advances (system description).
Christoph Redl. TPLP 16(5-6): 866-883 (2016).
http://www.kr.tuwien.ac.at/staff/redl/publications/r2016-tplp.pdf
Combining Answer Set Programming and domain heuristics for solving hard industrial problems.
Carmine Dodaro, Philip Gasteiger, Nicola Leone, Benjamin Musitsch, Francesco Ricca, Konstantin Schekotihin. TPLP 16(5-6): 653-669 (2016)
https://arxiv.org/pdf/1608.00730.pdf
External Propagators in WASP: Preliminary Report.
Carmine Dodaro, Francesco Ricca, and Peter Schüller. Proceedings of the 23rd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2016 (RCRA 2016). A workshop of the XV International Conference of the Italian Association for Artificial Intelligence (AI*IA 2016).
http://ceur-ws.org/Vol-1745/paper1.pdf
DLVHex:
Problem Solving Using the HEX Family.
Thomas Eiter, Christoph Redl, Peter Schüller. Computational Models of Rationality 2016: 150-174 (2016)
http://www.kr.tuwien.ac.at/staff/redl/publications/ers2016-festschrift.pdf
Exploiting Partial Assignments for Efficient Evaluation of Answer Set Programs with External Source Access.
Thomas Eiter, Tobias Kaminski, Christoph Redl, Antonius Weinzierl. IJCAI 2016: 1058-1065 (2016)
https://www.ijcai.org/Proceedings/16/Papers/154.pdf
A model building framework for answer set programming with external computations.
Thomas Eiter, Michael Fink, Giovambattista Ianni, Thomas Krennwallner, Christoph Redl, Peter Schüller. TPLP 16(4): 418-464 (2016)
http://www.kr.tuwien.ac.at/research/reports/rr1501.pdf
Efficient HEX-Program Evaluation Based on Unfounded Sets.
Thomas Eiter, Michael Fink, Thomas Krennwallner, Christoph Redl, Peter Schüller. J. Artif. Intell. Res. (JAIR) 49: 269-321 (2014)
https://www.jair.org/media/4175/live-4175-7717-jair.pdf
Conflict-driven ASP solving with external sources.
Thomas Eiter, Michael Fink, Thomas Krennwallner, Christoph Redl. TPLP 12(4-5): 659-679 (2012)
http://www.kr.tuwien.ac.at/staff/redl/publications/efkr2012-tplp.pdf
Potassco:
Modeling and Language Extensions.
Martin Gebser, Torsten Schaub. AI Magazine 37(3): 33-44 (2016)
http://www.cs.uni-potsdam.de/wv/pdfformat/gebsch16a.pdf
Clingo = ASP + Control: Preliminary Report.
Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. arxiv 2014. (2014)
http://www.cs.uni-potsdam.de/wv/pdfformat/gekakasc14b.pdf
https://arxiv.org/pdf/1405.3694v1.pdf
Ricochet Robots Reloaded. A Case-study in Multi-shot ASP Solving.
Martin Gebser, Roland Kaminski, Philipp Obermeier, and Torsten Schaub. Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation 2015: 17-32 (2015)
http://www.cs.uni-potsdam.de/wv/pdfformat/gekaobsc15a.pdf
For demos, the API ducumentation is here:
https://potassco.org/clingo/python-api/current/clingo.html
https://potassco.org/clingo/c-api/current/
IDP:
Predicate Logic as a Modelling Language: The IDP System.
Broes de Cat, Bart Bogaerts, Maurice Bruynooghe, Marc Denecker. CoRR abs/1401.6312 (2014).
http://www.bartbogaerts.eu/articles/future/a002/IDP.pdf
Visualising interactive inferences with IDPD3.
Ruben Lapauw, Ingmar Dasseville, Marc Denecker. CoRR abs/1511.00928 (2015)
https://arxiv.org/pdf/1511.00928.pdf
Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3.
Maurice Bruynooghe, Hendrik Blockeel, Bart Bogaerts, Broes de Cat, Stef De Pooter, Joachim Jansen, Anthony Labarre, Jan Ramon, Marc Denecker, Sicco Verwer. TPLP 15(6): 783-817 (2015)
https://lirias.kuleuven.be/bitstream/123456789/448838/1/journal.pdf
Other topics:
TDB