Lab for Automated Reasoning and Analysis LARA

Our publications

Note: you can search for LARA publications on Infoscience

2017

Proactive Synthesis of Recursive Tree-to-String Functions from Examples.

M. Mayer, V. Kuncak and J. Hamza.

European Conference on Object-Oriented Programming, Barcelona, Spain, Sun 18 - Fri 23 June 2017.

On verifying causal consistency.

A. Bouajjani, C. Enea, R. Guerraoui and J. Hamza.

44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, January, 15-21, 2017.

Programmation Interactive par l'Exemple.

M. Mayer.

Publish PhD Defense of Mikaël Mayer, EPFL, Lausanne, Switzerland, September 28, 2017.

2016

SMT-Based Checking of Predicate-Qualified Types for Scala.

G. S. Schmid and V. Kuncak.

7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016.

A Scala Library for Testing Student Assignments on Concurrent Programming.

M. Mayer and R. Madhavan.

7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016.

2015

Synthesizing Java Expressions from Free-Form Queries.

T. Gvero and V. Kuncak.

ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015.

Automating Grammar Comparison.

R. Madhavan, M. Mayer, S. Gulwani and V. Kuncak.

ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015.

Programming with Enumerable Sets of Structures.

I. Kuraj, V. Kuncak and D. Jackson.

ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015.

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.

T. Liang, N. Tsiskaridze, A. Reynolds, C. Tinelli and C. Barrett.

10th International Symposium on Frontiers of Combining Systems (FroCoS), Wroclaw, POLAND, SEP 21-24, 2015.Lecture Notes in Artificial Intelligence.

Developing Verified Software Using Leon.

V. Kuncak.

7th NASA Formal Methods Symposium (NFM), Pasadena, CA, APR 27-29, 2015.Lecture Notes in Computer Science.

Synthesizing Functions from Relations in Leon.

V. Kuncak, E. Kneuss and E. Koukoutos.

24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Univ Kent, Canterbury, ENGLAND, SEP 09-11, 2014.Lecture Notes in Computer Science.

A Decision Procedure for (Co)datatypes in SMT Solvers.

A. Reynolds and J. C. Blanchette.

25th International Conference on Automated Deduction (CADE), Berlin, GERMANY, AUG 01-07, 2015.Lecture Notes in Artificial Intelligence.

Induction for SMT Solvers.

A. Reynolds and V. Kuncak.

16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Mumbai, INDIA, JAN 12-14, 2015.Lecture Notes in Computer Science.

Interactive Synthesis using Free-Form Queries.

T. Gvero and V. Kuncak.

International Conference on Software Engineering, Demo Papers (ICSE Demo 2015), Florence, Italy, May 16-24, 2015.

On recursion-free Horn clauses and Craig interpolation.

P. Rummer, H. Hojjat and V. Kuncak.

in Formal Methods In System Design, vol. 47, num. 1, p. 1-25, 2015.

2014

Verifying and Synthesizing Software with Recursive Functions (Invited Contribution).

V. Kuncak.

41st International Colloquium on Automata, Languages and Programming.Lecture Notes in Computer Science.

Sound Compilation of Reals.

E. Darulova and V. Kuncak.

41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)', u'41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).

Modularity in the design of robust distributed algorithms.

G. Losa; R. Guerraoui and V. Kuncak (Dirs.).

EPFL, Lausanne.

2013

Game Programming by Demonstration.

V. Kuncak and M. Mayer.

Onward! 2013, Indianapolis, Indiana, USA, October 2013.

Interpolation for Synthesis on Unbounded Domains.

V. Kuncak and R. Blanc.

13th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, OCT 20-23, 2013.

An overview of the Leon verification system: verification by translation to recursive functions.

R. Blanc, E. Kneuss, V. Kuncak and P. Suter.

SCALA 2013, Montpellier, France, 2013.

Effect Analysis for Programs with Callbacks.

E. Kneuss, V. Kuncak and P. Suter.

Verified Software: Theories, Tools, Experiments, Menlo Park, CA, USA, 2013.Lecture Notes in Computer Science 8164.

Complete Completion using Types and Weights.

T. Gvero, V. Kuncak, I. Kuraj and R. Piskac.

34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)', u'34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).

Synthesis of Fixed-Point Programs.

E. Darulova, V. Kuncak, I. Saha and R. Majumdar.

International Conference on Embedded Software (EMSOFT), Montreal, Canada, Sept 29 - Oct 04, 2013.

CafeSat: a Modern SAT Solver for Scala.

R. W. Blanc.

the 4th Scala Workshop, Montpellier, France, 02 07 2013.

Automatic Synthesis of Out-of-Core Algorithms.

I. Klonatos, A. Nötzli, A. Spielmann, C. Koch and V. Kuncak.

ACM SIGMOD International Conference on Management of Data, New York, NY, USA, June 22-27, 20013.

Functional synthesis for linear arithmetic and sets.

V. Kuncak, M. Mayer, R. Piskac and P. Suter.

in International Journal on Software Tools for Technology Transfer, vol. 15, num. 5, p. 455–474, 2013.

Software verification and graph similarity for automated evaluation of students' assignments.

M. Vujosevic-Janicic, M. Nikolic, D. Tosic and V. Kuncak.

in Information And Software Technology, vol. 55, num. 6, p. 1004-1016, 2013.

Techniques for Program Synthesis.

R. W. Blanc.

2013.

2012

Certifying Solutions for Numerical Constraints.

E. Darulova and V. Kuncak.

Third International Conference on Runtime Verification, Istanbul, Turkey, September 25-28, 2012.

A Verification Toolkit for Numerical Transition Systems.

H. Hojjat, F. Konecny, F. Garnier, R. Iosif, V. Kuncak and P. Rummer.

18th International Symposium on Formal Methods, Paris, France, August 27-31, 2012.

Accelerating Interpolants.

H. Hojjat, R. Iosif, F. Konecny, V. Kuncak and P. Rummer.

10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, India, October 3-6, 2012.

Constraints as Control.

A. S. Koeksal, V. Kuncak and P. Suter.

39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, Jan 25-27, 2012.

Abortable Linearizable Modules.

R. Guerraoui, V. Kuncak and G. Losa.

in Archive of Formal Proofs (AFP), 2012.

Speculative Linearizability.

R. Guerraoui, V. Kuncak and G. Losa.

in Acm Sigplan Notices, vol. 47, num. 6, p. 55-66, 2012.

Symbolic execution of Reo circuits using constraint automata.

B. Pourvatan, M. Sirjani, H. Hojjat and F. Arbab.

in Science Of Computer Programming, vol. 77, p. 848-869, 2012.

Constraints as Control.

A. S. Koeksal, V. Kuncak and P. Suter.

in Acm Sigplan Notices (POPL), vol. 47, p. 151-164, 2012.

Software Synthesis Procedures.

V. Kuncak, M. Mayer, R. Piskac and P. Suter.

in Communications of the ACM, vol. 55, p. 103-111, 2012.

2011

Scala to the Power of Z3: Integrating SMT and Programming.

A. S. Koeksal, V. Kuncak and P. Suter.

23rd International Conference on Automated Deduction (CADE 23).Lecture Notes in Artificial Intelligence.

Decision Procedures for Automating Termination Proofs.

R. Piskac and T. Wies.

12th International Conference on Verification, Model Checking, and Abstract Interpretation, Austin, TX, Jan 23-25, 2011.Lecture Notes in Computer Science.

Trustworthy Numerical Computation in Scala.

E. Darulova and V. Kuncak.

ACM Conf. on Object-Oriented Programming, Systems, Languages, and Applications, Portland, Oregon, USA, October 25-27.

Towards Complete Reasoning about Axiomatic Specifications.

S. Jacobs and V. Kuncak.

Verification, Model Checking, and Abstract Interpretation (VMCAI).Lecture Notes in Computer Science.

Sets with Cardinality Constraints in Satisfiability Modulo Theories.

P. Suter, R. Steiger and V. Kuncak.

Verification, Model Checking, and Abstract Interpretation (VMCAI).Lecture Notes in Computer Science.

Interactive Synthesis of Code Snippets.

T. Gvero, V. Kuncak and R. Piskac.

Computer Aided Verification (CAV), 2011.

Scala to the Power of Z3: Integrating SMT and Programming.

A. S. Köksal, P. Suter and V. Kuncak.

Computer-Aideded Deduction (CADE).

Satisfiability Modulo Recursive Programs.

P. Suter, A. S. Köksal and V. Kuncak.

Static Analysis Symposium (SAS), 2011.Lecture Notes in Computer Science.

Measuring shape rectangularity.

D. Zunic and J. Zunic.

in Electronics Letters, vol. 47, p. 441-U102, 2011.

Formal Analysis of SystemC Designs in Process Algebra.

H. Hojjat, M. R. Mousavi and M. Sirjani.

in Fundamenta Informaticae, vol. 107, p. 19-42, 2011.

2010

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis.

E. Kneuss, P. Suter and V. Kuncak.

Runtime Veritication, St. Julians, Malta, November 1-4, 2010.

Phantm: PHP analyzer for type mismatch.

E. Kneuss, P. Suter and V. Kuncak.

FSE '10 Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, Santa-Fe, NM, USA, November 7-11 2010.

Ordered Sets in the Calculus of Data Structures.

V. Kuncak, R. Piskac and P. Suter.

Annual Conference of the European Association for Computer Science Logic, Brno, CZ, Aug 23-27, 2010.Lecture Notes in Computer Science.

Counterexample-Guided Focus.

A. Podelski and T. Wies.

37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Madrid, SPAIN, Jan 17-23, 2010.

Ordered Sets in the Calculus of Data Structures .

V. Kuncak, R. Piskac and P. Suter.

19th Annual Conference of the European Association for Computer Science Logic, Brno, Czech Republic, August 23-27, 2010.LNCS 6247.

MUNCH - Automated Reasoner for Sets and Multisets.

R. Piskac and V. Kuncak.

International Joint Conference on Automated Reasoning, Edinburgh, UK, July 16-19, 2010.LNCS 6173.

Building a Calculus of Data Structures .

V. Kuncak, R. Piskac, P. Suter and T. Wies.

11th International Conference on Verification, Model Checking and Abstract Interpretation, Madrid, Spain, January 17-19, 2010.LNCS 5944.

Comfusy: A Tool for Complete Functional Synthesis.

V. Kuncak, M. Mayer, R. Piskac and P. Suter.

22nd International Conference on Computer Aided Verification, Edinburgh, Scotland, UK, July 15-19, 2010.Lecture Notes in Computer Science 6174.

Phantm: PHP Analyzer for Type Mismatch.

E. Kneuss, P. Suter and V. Kuncak.

ACM SIGSOFT 18th International Symposium on the Foundations of Software Engineering, Santa Fe, New Mexico, USA, November 7-11, 2010.

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis.

E. Kneuss, P. Suter and V. Kuncak.

1st International Conference on Runtime Verification, St. Julians, Malta, November 1-4, 2010.Lecture Notes in Computer Science 6418.

Automatic Verification of Parametric Specifications with Complex Topologies.

J. Faber, C. Ihlemann, S. Jacobs and V. Sofronie-Stokkermans.

Integrated Formal Methods 2010, 8th International Conference, Nancy, France, October 11-14, 2010.

Decision Procedures for Algebraic Data Types with Abstractions.

P. Suter, M. Dotta and V. Kuncak.

ACM Symp. Principles of Programming Languages (POPL), 2010.

Test Generation through Programming in UDITA.

M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak and D. Marinov.

International Conference on Software Engineering (ICSE), 2010.

Complete Functional Synthesis.

V. Kuncak, M. Mayer, R. Piskac and P. Suter.

ACM Conf. Programming Language Design and Implementation (PLDI), 2010.

Predicting and Preventing Inconsistencies in Deployed Distributed Systems.

M. Yabandeh, N. Knezevic, D. Kostic and V. Kuncak.

in ACM Transactions on Computer Systems, vol. 28, num. 1, 2010.

On Deciding Functional Lists with Sublist Sets.

T. Wies, M. Marco and V. Kuncak.

2010.

2009

Combining Theories with Shared Set Operations.

T. Wies, R. Piskac and V. Kuncak.

7th International Symposium on Frontiers of Combining Systems, Trento, Italy, September 16-18, 2009.LNCS 5749.

Combining Theories with Shared Set Operations.

T. Wies, R. Piskac and V. Kuncak.

7th International Symposium on Frontiers of Combining Systems, Trento, ITALY, Sep 16-18, 2009.Lecture Notes in Artificial Intelligence.

Simplifying Distributed System Development.

M. Yabandeh, N. Vasić, D. Kostić and V. Kuncak.

12th Workshop on Hot Topics in Operating Systems.

An Integrated Proof Language for Imperative Programs.

K. Zee, V. Kuncak and M. Rinard.

ACM Conf. Programming Language Design and Implementation (PLDI).

Opis: Reliable Distributed Systems in OCaml.

P.-É. Dagand, D. Kostić and V. Kuncak.

ACM SIGPLAN Workshop on Types in Language Design and Implementation.

2008

Runtime Checking for Separation Logic.

H. H. Nguyen, V. Kuncak and W. N. Chin.

9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), San Francisco, USA, January 7-9, 2008.LNCS 4905.

Linear Arithmetic with Stars.

R. Piskac and V. Kuncak.

20th International Conference on Computed-Aided Verification (CAV), Princeton, NJ, USA, July 7-14, 2008.LNCS 5123.

Full Functional Verification of Linked Data Structures.

K. Zee, V. Kuncak and M. Rinard.

ACM Conf. Programming Language Design and Implementation (PLDI).

Decision Procedures for Multisets with Cardinality Constraints.

R. Piskac and V. Kuncak.

9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), San Francisco, January 2008.LNCS .

Constraint Solving for Software Reliability and Text Analysis.

V. Kuncak.

2008.

2007

Runtime Checking for Program Verification.

K. Zee, M. Taylor and M. Rinard.

Runtime Verification, Vancover, Canada, March 13, 2007.LNCS 4839.

Runtime Checking for Program Verification Systems.

K. Zee, V. Kuncak and M. Rinard.

Verifying Complex Properties using Symbolic Shape Analysis.

T. Wies, V. Kuncak, K. Zee, A. Podelski and M. Rinard.

Modular Data Structure Verification.

V. Kuncak.

See also Master's theses:

 
publications2.txt · Last modified: 2010/12/14 16:55 by wikiadmin