-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.bib
3768 lines (3511 loc) · 185 KB
/
main.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
@article{DBLP:journals/jar/PhamGW16,
author = {Tuan{-}Hung Pham and
Andrew Gacek and
Michael W. Whalen},
title = {Reasoning About Algebraic Data Types with Abstractions},
journal = {J. Autom. Reason.},
volume = {57},
number = {4},
pages = {281--318},
year = {2016},
doi = {10.1007/s10817-016-9368-2},
}
@inproceedings{DBLP:conf/cade/Sofronie-Stokkermans09,
author = {Viorica Sofronie{-}Stokkermans},
editor = {Renate A. Schmidt},
title = {Locality Results for Certain Extensions of Theories with Bridging
Functions},
booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5663},
pages = {67--83},
publisher = {Springer},
year = {2009},
doi = {10.1007/978-3-642-02959-2\_5},
}
@Book{Okasaki98PurelyFunctionalDataStructures,
author = {Chris Okasaki},
title = {Purely Functional Data Structures},
publisher = {Cambridge University Press},
year = 1998
}
@inproceedings{DBLP:conf/fm/Kassios06,
author = {Ioannis T. Kassios},
editor = {Jayadev Misra and
Tobias Nipkow and
Emil Sekerinski},
title = {Dynamic Frames: Support for Framing, Dependencies and Sharing Without
Restrictions},
booktitle = {{FM} 2006: Formal Methods, 14th International Symposium on Formal
Methods, Hamilton, Canada, August 21-27, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4085},
pages = {268--283},
publisher = {Springer},
year = {2006},
doi = {10.1007/11813040\_19},
}
@inproceedings{DBLP:conf/lpar/Leino10b,
author = {K. Rustan M. Leino},
editor = {Edmund M. Clarke and
Andrei Voronkov},
title = {Dafny: An Automatic Program Verifier for Functional Correctness},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 16th
International Conference, LPAR-16, Dakar, Senegal, April 25-May 1,
2010, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {6355},
pages = {348--370},
publisher = {Springer},
year = {2010},
doi = {10.1007/978-3-642-17511-4\_20},
}
@MastersThesis{antognini17genc,
author = {Marco Antognini},
title = {Extending Safe {C} Support in {L}eon},
school = {EPFL},
url = {https://infoscience.epfl.ch/record/227942/},
year = 2017}
@misc{surveys,
author = {Stack Overflow},
title = {Annual Developer Survey},
year = {2021},
url = {https://insights.stackoverflow.com/survey/}
}
@inproceedings{DBLP:conf/ijcai/BoyerM73,
author = {Robert S. Boyer and
J. Strother Moore},
editor = {Nils J. Nilsson},
title = {Proving Theorems about {LISP} Functions},
booktitle = {Proceedings of the 3rd International Joint Conference on Artificial
Intelligence. Standford, CA, USA, August 20-23, 1973},
pages = {486--493},
publisher = {William Kaufmann},
year = {1973},
url = {http://ijcai.org/Proceedings/73/Papers/053.pdf},
}
@article{More2019milestones,
author = {J. Strother Moore},
title = {Milestones from the Pure Lisp theorem prover to {ACL2}},
journal = {Formal Aspects Comput.},
volume = {31},
number = {6},
pages = {699--732},
year = {2019},
doi = {10.1007/s00165-019-00490-3},
}
@inproceedings{DBLP:conf/pldi/HallahanXBJP19,
author = {William T. Hallahan and
Anton Xue and
Maxwell Troy Bland and
Ranjit Jhala and
Ruzica Piskac},
editor = {Kathryn S. McKinley and
Kathleen Fisher},
title = {Lazy counterfactual symbolic execution},
booktitle = {Proceedings of the 40th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2019, Phoenix, AZ, USA,
June 22-26, 2019},
pages = {411--424},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3314221.3314618},
doi = {10.1145/3314221.3314618},
}
@inproceedings{pluscal,
author = {Leslie Lamport},
editor = {Martin Leucker and
Carroll Morgan},
title = {The PlusCal Algorithm Language},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2009, 6th International
Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5684},
pages = {36--60},
publisher = {Springer},
year = {2009},
doi = {10.1007/978-3-642-03466-4\_2},
}
@phdthesis{vazou2016liquid,
title={Liquid Haskell: Haskell as a Theorem Prover},
author={Vazou, Niki},
year={2016},
school={UNIVERSITY OF CALIFORNIA, SAN DIEGO}
}
@inproceedings{kind2,
author = {Adrien Champion and
Alain Mebsout and
Christoph Sticksel and
Cesare Tinelli},
title = {The Kind 2 Model Checker},
booktitle = {Computer Aided Verification - 28th International Conference, {CAV}
2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {9780},
pages = {510--517},
publisher = {Springer},
year = {2016},
doi = {10.1007/978-3-319-41540-6\_29},
}
@phdthesis{voirol2019,
title = {Verified Functional Programming},
author = {Nicolas Charles Yves Voirol},
year = {2019},
school = {EPFL, thesis number 9479},
url = {http://doi.org/10.5075/epfl-thesis-9479}
}
@phdthesis{blanc2017,
title = {Verification by Reduction to Functional Programs},
author = {R\'egis William Blanc},
year = {2017},
school = {EPFL, thesis number 7636},
url = {http://doi.org/10.5075/epfl-thesis-9479}
}
@misc{schmid2021proving,
title={Proving and Disproving Programs with Shared Mutable Data},
author={Georg Schmid and Viktor Kunčak},
year={2021},
eprint={2103.07699},
archivePrefix={arXiv},
primaryClass={cs.LO}
}
@Book{OderskyETAL20ProgrammingScala,
author = {Martin Odersky and Lex Spoon and Bill Venners},
title = {Programming in Scala},
edition = {4},
publisher = {Artima Inc},
date = {15 January},
isbn = {978-0981531618},
year = 2008
}
@InProceedings{EdelmannETAL20ZippyLLParsingDerivatives,
author = {Romain Edelmann and Jad Hamza and Viktor Kun\v{c}ak},
title = {Zippy {LL(1)} Parsing with Derivatives},
booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)},
year = 2020}
@Article{HamzaETAL19SystemFR,
author = {Jad Hamza and Nicolas Voirol and Viktor Kun\v{c}ak},
title = {{System FR}: Formalized Foundations for the {Stainless} Verifier},
journal = {Proc. ACM Program. Lang},
number = {OOPSLA},
year = {2019},
month = {November},
doi = {https://doi.org/10.1145/3360592}
}
@inproceedings{HamzaKuncak19MinimalSynthesis,
author = {Jad Hamza and Viktor Kun\v{c}ak},
title = {Minimal Synthesis of String to String Functions from Examples},
booktitle = {Verification, Model Checking, and Abstract Interpretation ({VMCAI})},
pages = {48--69},
year = {2019},
doi = {10.1007/978-3-030-11245-5\_3},
}
@Article{MayerETAL18BidirectionalEvaluation,
author = {Mika\"el Mayer and Viktor Kun\v{c}ak and Ravi Chugh},
title = {Bidirectional Evaluation with Direct Manipulation},
journal = {Proc. ACM Program. Lang},
number = {OOPSLA, Article 127},
year = {2018},
month = {November},
}
@Article{ReynoldsETAL17SolvingQuantified,
author = {Andrew Reynolds and Tim King and Viktor Kuncak},
title = {Solving quantified linear arithmetic by counterexample-guided instantiation},
journal = {Formal Methods in System Design (FMSD)},
year = 2017}
@Article{ReynoldsETAL17RefutationSMT,
author = {Andrew Reynolds and Viktor Kuncak and Cesare Tinelli and Clark Barrett and Morgan Deters},
title = {Refutation-based synthesis in {SMT}},
journal = {Formal Methods in System Design (FMSD)},
year = 2017}
@InProceedings{MayerETAL17ProactiveSynthesis,
author = {Mika{\"e}l Mayer and Jad Hamza and Viktor Kuncak},
title = {{Proactive Synthesis of Recursive Tree-to-String Functions from Examples}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {19:1--19:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {Peter M{\"u}ller},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7257},
URN = {urn:nbn:de:0030-drops-72575},
doi = {10.4230/LIPIcs.ECOOP.2017.19},
annote = {Keywords: programming by example, active learning, program synthesis}
}
@article{DarulovaKuncak17RealsTOPLAS,
author = {Darulova, Eva and Kuncak, Viktor},
title = {Towards a Compiler for Reals},
journal = {ACM Trans. Program. Lang. Syst. (TOPLAS)},
issue_date = {March 2017},
volume = {39},
number = {2},
month = {March},
year = {2017},
issn = {0164-0925},
pages = {8:1--8:28},
articleno = {8},
numpages = {28},
doi = {10.1145/3014426},
publisher = {ACM},
address = {New York, NY, USA},
}
@InProceedings{MadhavanKuncak17Memoization,
author = {Ravichandhran Madhavan and Sumith Kulal and Viktor Kuncak},
title = {Contract-Based Resource Verification for Higher-order Functions with Memoization},
booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
year = 2017}
@InProceedings{SchmidKuncak16CheckingPredicate,
author = {Georg Stefan Schmid and Viktor Kuncak},
title = {{SMT}-Based Checking of Predicate-Qualified Types for {S}cala},
booktitle = {Scala Symposium},
year = 2016}
@InProceedings{KoukoutosETAL16UpdateDeductiveSynthesisRepairLeonTool,
author = {Manos Koukoutos and Etienne Kneuss and Viktor Kuncak},
title = {An Update on Deductive Synthesis and Repair in the Leon Tool},
booktitle = {5th Workshop on Synthesis},
year = 2016}
@InProceedings{HupelKuncak16TranslatingScalaProgramsIsabelleHOLSystemDescription,
author = {Lars Hupel and Viktor Kuncak},
title = {Translating Scala Programs to Isabelle/HOL (System Description)},
booktitle = {International Joint Conference on Automated Reasoning (IJCAR)},
year = 2016}
@InProceedings{KurajETAL15ProgrammingEnumerableSetsStructures,
author = {Ivan Kuraj and Viktor Kuncak and Daniel Jackson},
title = {Programming with Enumerable Sets of Structures},
booktitle = {OOPSLA},
year = 2015}
@InProceedings{GveroKuncak15SynthesizingJavaExpressionsFreeFormQueries,
author = {Tihomir Gvero and Viktor Kuncak},
title = {Synthesizing Java Expressions from Free-Form Queries},
booktitle = {OOPSLA},
year = 2015}
@InProceedings{MadhavanETAL15AutomatingGrammarComparison,
author = {Ravichandhran Madhavan and Mikael Mayer and Sumit Gulwani and Viktor Kuncak},
title = {Automating Grammar Comparison},
booktitle = {OOPSLA},
year = 2015}
@InProceedings{KneussETAL15DeductiveProgramRepair,
author = {Etienne Kneuss and Manos Koukoutos and Viktor Kuncak},
title = {Deductive Program Repair},
booktitle = {Computer-Aided Verification (CAV)},
year = 2015}
@InProceedings{ReynoldsETAL15CegisSMT,
author = {Andrew Reynolds and Morgan Deters and
Viktor Kuncak and Cesare Tinelli and Clark Barrett},
title = {Counterexample Guided Quantifier Instantiation for Synthesis in {SMT}},
booktitle = {Computer-Aided Verification (CAV)},
year = 2015}
@InProceedings{VoirolETAL15CounterExampleCompleteVerificationHigherOrderFunctions,
author = {Nicolas Voirol and Etienne Kneuss and Viktor Kuncak},
title = {Counter-Example Complete Verification for Higher-Order Functions},
booktitle = {Scala Symposium},
year = 2015}
@InProceedings{BlancKuncak15SoundReasoningIntegralDataTypes,
author = {R\'egis Blanc and Viktor Kuncak},
title = {Sound Reasoning about Integral Data Types with a Reusable {SMT} Solver Interface},
booktitle = {Scala Symposium},
year = 2015}
@InProceedings{GveroKuncak15InteractiveSynthesisUsingFreeForm,
author = {Tihomir Gvero and Viktor Kuncak},
title = {Interactive Synthesis Using Free-Form Queries (Tool Demonstration)},
booktitle = {International Conference on Software Engineering ({ICSE})},
year = 2015}
@InProceedings{Kuncak15DevelopingVerifiedSoftwareUsingLeonNFM,
author = {Viktor Kuncak},
title = {Developing Verified Software Using {Leon} (Invited Contribution)},
booktitle = {{NASA} Formal Methods (NFM)},
year = 2015}
@InProceedings{ReynoldsKuncak15InductionSMTSolvers,
author = {Andrew Reynolds and Viktor Kuncak},
title = {Induction for {SMT} Solvers},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
year = 2015}
@TechReport{ReynoldsKuncak14InductionSMTSolvers,
author = {Andrew Reynolds and Viktor Kuncak},
title = {On Induction for {SMT} Solvers},
institution = {EPFL},
year = 2014,
number = {EPFL-REPORT-201755}}
@TechReport{GveroKuncak14OnSynthesizingCodeFreeFormQueries,
author = {Tihomir Gvero and Viktor Kuncak},
title = {On Synthesizing Code from Free-Form Queries},
institution = {EPFL},
year = 2014,
number = {EPFL-REPORT-201606}}
@InProceedings{KuncakETAL14SynthesizingFunctionsRelationsLeon,
author = {Viktor Kuncak and Etienne Kneuss and Emmanouil Koukoutos},
title = {Synthesizing Functions from Relations in {Leon} (Invited Contribution)},
booktitle = {Logic-Based Program Synthesis and Transformation (LOPSTR)},
year = 2014}
@InProceedings{KurajKuncak14SciFe,
author = {Ivan Kuraj and Viktor Kuncak},
title = {SciFe: Scala Framework for Efficient Enumeration of Data Structures with Invariants},
booktitle = {Scala Workshop},
year = 2014}
@InProceedings{KoukoutosKuncak14CheckingDataStructurePropertiesOrdersMagnitudeFaster,
author = {Emmanouil Koukoutos and Viktor Kuncak},
title = {Checking Data Structure Properties Orders of Magnitude Faster},
booktitle = {Runtime Verification (RV)},
year = 2014}
@InProceedings{Kuncak14VerifyingSynthesizingSoftwareRecursiveFunctionsInvitedTalk,
author = {Viktor Kuncak},
title = {Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)},
booktitle = {41st International Colloquium on Automata, Languages, and Programming (ICALP)},
year = 2014}
@InProceedings{MadhavanKuncak14SymbolicResourceBoundInferenceFunctionalPrograms,
author = {Ravichandhran Madhavan and Viktor Kuncak},
title = {Symbolic Resource Bound Inference for Functional Programs},
booktitle = {Computer Aided Verification (CAV)},
year = 2014}
@TechReport{MadhavanKuncak13TemplateBasedInferenceRichInvariantsLeon,
author = {Ravichandhran Madhavan and Viktor Kuncak},
title = {On Template-Based Inference of Rich Invariants in {L}eon},
institution = {EPFL},
year = 2013,
number = {EPFL-REPORT-190578},
month = {November}}
@InProceedings{DarulovaKuncak14SoundCompilationReals,
author = {Eva Darulova and Viktor Kuncak},
title = {Sound Compilation of Reals},
booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
year = 2014}
@InProceedings{KneussETAL13SynthesisModuloRecursiveFunctions,
author = {Etienne Kneuss and Viktor Kuncak and Ivan Kuraj and Philippe Suter},
title = {Synthesis Modulo Recursive Functions},
booktitle = {OOPSLA},
year = 2013}
@InProceedings{MayerKuncak13GameProgrammingDemonstration,
author = {Mika\"el Mayer and Viktor Kuncak},
title = {Game Programming by Demonstration},
booktitle = {SPLASH Onward!},
year = 2013}
@InProceedings{KuncakBlanc13InterpolationSynthesisUnboundedDomains,
author = {Viktor Kuncak and R\'egis Blanc},
title = {Interpolation for Synthesis on Unbounded Domains},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
year = 2013}
@InProceedings{DarulovaETAL13SynthesisFixedPointPrograms,
author = {Eva Darulova and Viktor Kuncak and Rupak Majumdar and Indranil Saha},
title = {Synthesis of Fixed-Point Programs},
booktitle = {Embedded Software (EMSOFT)},
year = 2013}
@InProceedings{KneussETAL13EffectAnalysisProgramsCallbacks,
author = {Etienne Kneuss and Viktor Kuncak and Philippe Suter},
title = {Effect Analysis for Programs with Callbacks},
booktitle = {Fifth Working Conference on Verified Software: Theories, Tools and Experiments},
year = 2013}
@InProceedings{RuemmerETAL13ClassifyingSolvingHornClausesVerification,
author = {Philipp R\"ummer and Hossein Hojjat and Viktor Kuncak},
title = {Classifying and Solving Horn Clauses for Verification},
booktitle = {Fifth Working Conference on Verified Software: Theories, Tools and Experiments},
year = 2013}
@InProceedings{KuncakETAL13ExecutingSpecificationsSynthesisConstraintSolvingInvitedTalk,
author = {Viktor Kuncak and Etienne Kneuss and Philippe Suter},
title = {Executing Specifications using Synthesis and Constraint Solving (Invited Talk)},
booktitle = {Runtime Verification (RV)},
year = 2013}
@InProceedings{BlancETAL13VerificationTranslationRecursiveFunctions,
author = {R\'egis William Blanc and Etienne Kneuss and Viktor Kuncak and Philippe Suter},
title = {An Overview of the {Leon} Verification System: Verification by Translation to Recursive Functions},
booktitle = {Scala Workshop},
year = 2013
}
@InProceedings{SpielmannETAL13AutomaticSynthesisOutCoreAlgorithms,
author = {Andrej Spielmann and Andres N\"{o}tzli and Christoph Koch and Viktor Kuncak and Yannis Klonatos},
title = {Automatic Synthesis of Out-of-Core Algorithms},
booktitle = {SIGMOD},
year = 2013,
}
@TechReport{BlancETAL13OnVerificationTranslationRecursiveFunctions,
author = {R\'egis William Blanc and Etienne Kneuss and Viktor Kuncak and Philippe Suter},
title = {On Verification by Translation to Recursive Functions},
institution = {EPFL},
year = 2013,
number = {EPFL-REPORT-186233}}
@TechReport{KneussETAL13IntegratingDeductiveSynthesisVerificationSystems,
author = {Etienne Kneuss and Viktor Kuncak and Ivan Kuraj and Philippe Suter},
title = {On Integrating Deductive Synthesis and Verification Systems},
institution = {EPFL},
year = 2013,
number = {EPFL-REPORT-186043}}
@InProceedings{RuemmerETAL13DisjunctiveInterpolantsHornClauseVerification,
author = {Philipp R\"ummer and Hossein Hojjat and Viktor Kuncak},
title = {Disjunctive Interpolants for Horn-Clause Verification},
booktitle = {Computer Aided Verification (CAV)},
year = 2013}
@InProceedings{GveroETAL13CompleteCompletionTypesWeights,
author = {Tihomir Gvero and Viktor Kuncak and Ivan Kuraj and Ruzica Piskac},
title = {Complete Completion using Types and Weights},
booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)},
year = 2013}
@Article{Vujosevic-JanicicETAL13SoftwareVerificationGraphSimilarityAutomated,
author = {Milena Vujo\v{s}evi\'{c}-Jani\v{c}i\'{c} and Mladen Nikoli\'{c} and Du\v{s}an To\v{s}i\'{c} and Viktor Kuncak},
title = {Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments},
journal = {Information and Software Technology},
year = 2013}
@InProceedings{JacobsETAL13ReductionsSynthesisProcedures,
author = {Swen Jacobs and Viktor Kuncak and Phillippe Suter},
title = {Reductions for Synthesis Procedures},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
year = 2013,
abstract = {A synthesis procedure acts as a compiler for declarative
specifications. It accepts a formula describing a relation
between inputs and outputs, and generates a function
implementing this relation. This paper presents synthesis
procedures for data structures. Our procedures are
reductions that lift a synthesis procedure for the elements
into synthesis procedures for containers storing these
elements. We introduce a framework to describe synthesis
procedures as systematic applications of inference rules. We
show that, by interpreting both synthesis problems and
programs as relations, we can derive and modularly prove
transformation rules that are widely applicable, thus
simplifying both the presentation and the correctness
argument.}
}
@InProceedings{DarulovaKuncak12CertifyingSolutionsNumericalConstraints,
author = {Eva Darulova and Viktor Kuncak},
title = {Certifying Solutions for Numerical Constraints},
booktitle = {Runtime Verification (RV)},
year = 2012,
abstract={A large portion of software is used for numerical
computation in mathematics, physics and engineering. Among
the aspects that make verification in this domain difficult
is the need to quantify numerical errors, such as roundoff
errors and errors due to the use of approximate numerical
methods. Much of numerical software uses self-stabilizing
iterative algorithms, for example, to find solutions of
nonlinear equations. To support such algorithms, we present
a runtime verification technique that checks, given a
nonlinear equation and a tentative solution, whether this
value is indeed a solution to within a specified precision.
Our technique combines runtime verification approaches with
information about the analytical equation being solved. It
is independent of the algorithm used for finding the
solution and is therefore applicable to a wide range of
problems. We have implemented our technique for the Scala
programming language using our affine arithmetic library and
the macro facility of Scala 2.10.
}}
@InProceedings{HojjatETAL12AcceleratingInterpolants,
author = {Hossein Hojjat and Radu Iosif and
Filip Kone\v{c}n\'{y} and Viktor Kuncak and Philipp R\"ummer},
title = {Accelerating Interpolants},
booktitle = {Automated Technology for Verification and Analysis (ATVA)},
year = 2012,
abstract = {We present Counterexample-Guided Accelerated Abstraction
Refinement (CEGAAR), a new algorithm for verifying infinite-state
transition systems. CEGAAR combines interpolation-based predicate
discovery in counterexample-guided predicate abstraction with
acceleration technique for computing the transitive closure of
loops. CEGAAR applies acceleration to dynamically discovered
looping patterns in the unfolding of the transition system, and
combines overapproximation with underapproximation. It constructs
inductive invariants that rule out an infinite family of spurious
counterexamples, alleviating the problem of divergence in predicate
abstraction without losing its adaptive nature. We present theoretical
and experimental justification for the effectiveness of CEGAAR,
showing that inductive interpolants can be computed from classical
Craig interpolants and transitive closures of loops. We present an
implementation of CEGAAR that verifies integer transition
systems. We show that the resulting implementation robustly handles a
number of difficult transition systems that cannot be handled using
interpolation-based predicate abstraction or acceleration alone.}
}
@InProceedings{HojjatETAL12VerificationToolkitNTS,
author = {Hossein Hojjat and Filip Konecny and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp Ruemmer},
title = {A Verification Toolkit for Numerical Transition Systems (Tool Paper)},
booktitle = {16th International Symposium on Formal Methods (FM)},
year = 2012,
publisher = {Springer},
abstract = {This paper reports on an effort to create benchmarks and a toolkit for
rigorous verification problems, simplifying tool integration and
eliminating ambiguities of complex programming language constructs. We
focus on Integer Numerical Transition Systems (INTS), which can
be viewed as control-flow graphs whose edges are annotated by
Presburger arithmetic formulas. We describe the syntax, semantics, a
front-end, and a first release of benchmarks for such transition
systems. Furthermore, we present Flata and Eldarica,
two new verification tools for INTS. The Flata system is based on
precise acceleration of the transition relation, while the
Eldarica system is based on predicate abstraction with
interpolation-based counterexample-driven refinement. The
Eldarica verifier uses the Princess theorem prover
as a sound and complete interpolating prover for Presburger
arithmetic. Both systems can solve several examples for which previous
approaches failed and present a useful baseline for verifying integer
programs. Our infrastructure is publicly available; we hope that it
will spur further research, benchmarking, competitions, and
synergistic communication between verification tools.}}
@InProceedings{SpielmannKuncak12SynthesisUnboundedBitvectorArithmetic,
author = {Andrej Spielmann and Viktor Kuncak},
title = {Synthesis for Unbounded Bitvector Arithmetic},
booktitle = {International Joint Conference on Automated
Reasoning (IJCAR)},
year = 2012,
series = {LNAI},
publisher = {Springer},
abstract = {We propose to describe computations using QFPAbit, a language of quantifier-free linear arithmetic on unbounded integers with bitvector operations. We describe an algorithm that, given a QFPAbit formula with input and output variables denoting integers, generates an efficient function from a sequence of inputs to a sequence of outputs, whenever such function on integers exists. The starting point for our method is a polynomial-time translation mapping a QFPAbit formula into the sequential circuit that checks the correctness of the input/output relation. From such a circuit, our synthesis algorithm produces solved circuits from inputs to outputs that are no more than singly exponential in size of the original formula. In addition to the general synthesis algorithm, we present techniques that ensure that, for example, multiplication and division with large constants do not lead to an exponential blowup, addressing a practical problem with a previous approach that used the MONA tool to generate the specification automata.}}
@InProceedings{GuerraouiETAL12SpeculativeLinearizability,
author = {Rachid Guerraoui and Viktor Kuncak and Giuliano Losa},
title = {Speculative Linearizability},
booktitle = {ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)},
abstract = {Linearizability is a key design methodology for reasoning
about implementations of concurrent abstract data types in
both shared memory and message passing systems. It provides
the illusion that operations execute sequentially and
fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed
one. A key property of linearizability is inter-object
composability: a system composed of linearizable objects is itself linearizable.
However, devising linearizable objects is very
difficult, requiring complex algorithms to work
correctly under general circumstances, and often resulting
in bad average-case behavior. Concurrent algorithm
designers therefore resort to speculation: optimizing algorithms
to handle common scenarios more efficiently.
The outcome are even more complex protocols, for which it is
no longer tractable to prove their correctness.
To simplify the design of efficient yet robust linearizable protocols,
we propose a new notion: \emph{speculative linearizability}. This property is as general as
linearizability, yet it allows intra-object composability: the correctness of independent protocol phases implies the correctness of their composition.
In particular,
it allows the designer to focus solely on the proof of
an optimization and derive the
correctness of the overall protocol from the correctness of
the existing, non-optimized one.
Our notion of protocol phases allows
processes to independently switch from one phase to another,
without requiring them to reach agreement
to determine the change of a phase.
To illustrate the
applicability of our methodology, we show how
examples of speculative algorithms for shared memory and
asynchronous message passing naturally
fit into our framework.
We rigorously define
speculative linearizability and prove our intra-object composition
theorem in a trace-based
as well as an automaton-based model.
To obtain a further degree of confidence, we also
formalize and mechanically
check the theorem in the automaton-based model, using
the I/O automata framework within the Isabelle interactive proof assistant.},
year = 2012}
@Article{KuncakETAL12SoftwareSynthesisProcedures,
author = {Viktor Kuncak and Mika\"el Mayer and Ruzica Piskac and Philippe Suter},
title = {Software Synthesis Procedures},
journal = {Communications of the ACM},
date = {February},
year = 2012,
abstract = {Automated synthesis of program fragments from specifications
can make programs easier to write and easier to reason about. To integrate
synthesis into programming languages software synthesis algorithms should
behave in a predictable way: they should succeed for a well-defined class of
specifications. We propose to systematically generalize decision procedures
into synthesis procedures, and use them to compile implicitly specified
computations embedded inside functional and imperative programs. Synthesis
procedures are predictable, because they are guaranteed to find code that
satisfies the specification whenever such code exists. To illustrate our
method, we derive synthesis procedures by extending quantifier elimination
algorithms for integer arithmetic and set data structures. We then show that
an implementation of such synthesis procedures can extend a compiler to
support implicit value definitions and advanced pattern matching.}
}
@Article{KuncakETAL12FunctionalSynthesisLinearArithmeticSets,
author = {Viktor Kuncak and Mikael Mayer and Ruzica Piskac and Philippe Suter},
title = {Functional Synthesis for Linear Arithmetic and Sets},
journal = {Software Tools for Technology Transfer (STTT)},
year = 2012,
abstract = {Synthesis of program fragments from specifications can make
programs easier to write and easier to reason about. To
integrate synthesis into programming languages, synthesis
algorithms should behave in a predictable way---they should
succeed for a well-defined class of specifications.
To guarantee correctness and applicability to software
(and not just hardware), these algorithms
should also support unbounded data types, such as numbers and
data structures.
To obtain appropriate synthesis algorithms, we propose to generalize decision
procedures into predictable and complete synthesis
procedures. Such procedures are guaranteed to find code that
satisfies the specification if such code exists. Moreover,
we identify conditions under which synthesis will statically
decide whether the solution is guaranteed to exist, and
whether it is unique. We demonstrate our approach by
starting from a quantifier elimination decision procedure for Boolean Algebra
of set with Presburger Arithmetic (BAPA) and transforming it
into a synthesis procedure. Our procedure also works in the presence
of parametric coefficients. We establish results on the size and the
efficiency of the synthesized code. We show that such
procedures are useful as a language extension with implicit
value definitions, and we show how to extend a compiler to
support such definitions. Our constructs provide the
benefits of synthesis to programmers, without requiring them
to learn new concepts, give up a deterministic execution
model, or provide code skeletons.},
volume = {TBD},
number = {TBD}}
@InProceedings{WiesETAL12DecidingFunctionalListswithSublistSets,
author = {Thomas Wies and Marco Mu\~niz and Viktor Kuncak},
title = {Deciding Functional Lists with Sublist Sets},
booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
year = 2012,
series = {LNCS},
abstract = {Motivated by the problem of deciding verification conditions
for the verification of functional programs, we present new decision
procedures for automated reasoning about functional lists. We first
show how to decide in NP the satisfiability problem for logical
constraints containing equality, constructor, selectors, as well
as the transitive sublist relation. We then extend this class of
constraints with operators to compute the set of all sublists, and
the set of objects stored in a list. Finally, we support constraints
on sizes of sets, which gives us the ability to compute list length
as well as the number of distinct list elements. We show that the
extended theory is reducible to the theory of sets with linear
cardinality constraints, and therefore still in NP. This reduction
enables us to combine our theory with other decidable theories that
impose constraints on sets of objects, which further increases the
potential of our decidability result in verification of functional
and imperative software.
}}
@InProceedings{VujosevicJanicicKuncak12DevelopmentandEvaluationofLAV,
author = {Milena Vujo\v{s}evi\'{c}-Jani\v{c}i\'{c} and Viktor Kuncak},
title = {Development and Evaluation of {LAV}: an {SMT}-Based Error Finding Platform},
booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
year = 2012,
series = {LNCS},
abstract = {We present design and evaluation of LAV, a new open-source tool
for statically checking program assertions and errors. LAV integrates into
the popular LLVM infrastructure for compilation and analysis. LAV uses symbolic execution to construct a first-order logic formula that models the behavior
of each basic blocks. It models the relationships between basic blocks using
propositional formulas. By combining these two kinds of formulas LAV generates
polynomial-sized verification conditions for loop-free code. It uses
underapproximating or overapproximating unrolling to handle loops. LAV can
pass generated verification conditions to one of the several SMT solvers:
Boolector, MathSAT, Yices, and Z3. Our experiments with small 200 benchmarks
suggest that LAV is competitive with related tools, so it can be used as an
effective alternative for certain verification tasks. The experience also
shows that LAV provides significant help in analyzing student programs and providing feedback to students in everyday university practice.}
}
@InProceedings{KoeksalETAL12ConstraintsControl,
author = {{Ali Sinan} K\"oksal and Viktor Kuncak and Philippe Suter},
title = {Constraints as Control},
booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
abstract = {
We present an extension of Scala that supports constraint
programming over bounded and unbounded domains. The
resulting language, Kaplan, provides the benefits of
constraint programming while
preserving the existing features of Scala. Kaplan integrates
constraint and imperative programming by using constraints
as an advanced control structure; the developers
use the monadic 'for' construct to iterate over the
solutions of constraints or branch on the existence of a
solution.
The constructs we introduce have simple
semantics that can be understood as explicit
enumeration of values, but are implemented more efficiently using
symbolic reasoning.
Kaplan programs can manipulate constraints at run-time, with the combined benefits
of type-safe syntax trees and first-class functions.
The language of constraints is
a functional subset of Scala, supporting arbitrary recursive
function definitions over algebraic data types, sets, maps,
and integers.
Our implementation runs on a platform
combining a constraint solver with a standard virtual
machine. For constraint solving we use an algorithm that
handles recursive function definitions through
fair function unrolling and builds upon
the state-of-the art SMT solver Z3.
We evaluate Kaplan on examples ranging
from enumeration of data structures to execution of
declarative specifications.
We found Kaplan promising
because it is expressive, supporting a range of problem domains,
while enabling full-speed execution
of programs that do not rely on constraint programming.
},
year = 2012}
@InProceedings{DarulovaKuncak11TrustworthyNumericalComputationinScala,
author = {Eva Darulov\'a and Viktor Kuncak},
title = {Trustworthy Numerical Computation in Scala},
booktitle = {OOPSLA},
abstract = {
Modern computing has adopted the floating point type as a default way to describe computations with real
numbers. Thanks to dedicated hardware support, such computations are efficient on modern architectures, even in double precision.
However, rigorous reasoning about the resulting programs remains difficult.
This is in part due to a large gap between
the finite floating point representation and the infinite-precision real-number semantics that serves as the developers' mental
model. Because programming languages do not provide support for estimating errors,
some computations in practice are performed more and some less precisely than needed.
We present a library solution for rigorous arithmetic computation. Our numerical data type library tracks a (double)
floating point value, but also a guaranteed upper bound on the error between this value and the ideal value that
would be computed in the real-value semantics. Our implementation involves
a set of linear approximations based on an extension of affine arithmetic. The derived approximations
cover most of the standard mathematical operations, including trigonometric functions, and are more comprehensive
than any publicly available ones.
Moreover, while interval arithmetic
rapidly yields overly pessimistic estimates, our approach remains precise for several computational tasks of interest.
We evaluate the library on a number of examples from numerical analysis and physical simulations. We found it to be a useful tool
for gaining confidence in the correctness of the computation.
},
year = 2011}
@InProceedings{SuterETAL11SatisfiabilityModuloRecursivePrograms,
author = {Philippe Suter and Ali Sinan K\"{o}ksal and Viktor Kuncak},
title = {Satisfiability Modulo Recursive Programs},
booktitle = {Static Analysis Symposium (SAS)},
year = 2011,
abstract = {We present a semi-decision procedure for checking expressive
correctness properties of recursive first-order functional
programs. In our approach, both properties and programs are
expressed in the same language, which is a subset of Scala.
We have implemented our procedure and integrated it with the
Z3 SMT solver and the Scala compiler. Our procedure is sound
for proofs and counterexamples. It is terminating
and thus complete for many important classes of
specifications, including 1) all verification problems
containing counterexamples, 2) functions annotated with
inductive postconditions, and 3) abstraction functions and
invariants of recursive data types that commonly arise in
functional programs. Using our system, we verified detailed correctness
properties for functional data structure implementations, as well as Scala
syntax tree manipulations. We have found our system to be fast for both
finding counterexamples and finding correctness proofs, and to scale to
larger programs than alternative techniques.
}}
@InProceedings{WiesETAL11EfficientDecisionProcedureforImperative,
author = {Thomas Wies and Marco {Mu\~{n}iz} and Viktor Kuncak},
title = {An Efficient Decision Procedure for Imperative Tree Data Structures},
booktitle = {Computer-Aideded Deduction (CADE)},
abstract = {
We present a new decidable logic called TREX for expressing
constraints about imperative tree data structures. In particular,
TREX supports a transitive closure operator that can express
reachability constraints, which often appear in data structure
invariants. We show that our logic is closed under weakest
precondition computation, which enables its use for automated
software verification. We further show that satisfiability of
formulas in TREX is decidable in NP. The low complexity makes it an
attractive alternative to more expensive logics such as monadic
second-order logic (MSOL) over trees, which have been traditionally
used for reasoning about tree data structures.
},
year = 2011}
@InProceedings{KoeksalETAL11ScalaZ3,
author = {{Ali Sinan} K{\"o}ksal and Viktor Kuncak and Philippe Suter},
title = {Scala to the Power of {Z3}: Integrating {SMT} and Programming},
booktitle = {Computer-Aideded Deduction (CADE) Tool Demo},
abstract = {
We describe a system that integrates the SMT solver Z3 with the Scala
programming language. The system supports the use of the SMT solver for
checking satisfiability, unsatisfiability, as well as solution enumeration. The
embedding of formula trees into Scala uses the host type system of Scala to
prevent the construction of certain ill-typed constraints. The solution
enumeration feature integrates into the iteration constructions of Scala and
supports writing non-deterministic programs. Using Z3's mechanism of theory
extensions, our system also helps users construct custom constraint solvers
where the interpretation of predicates and functions is given as Scala code.
The resulting system preserves the productivity advantages of Scala while
simplifying tasks such as combinatorial search.
},
year = 2011}
@InProceedings{GveroETAL11InteractiveSynthesisofCodeSnippets,
author = {Tihomir Gvero and Viktor Kuncak and Ruzica Piskac},
title = {Interactive Synthesis of Code Snippets},
booktitle = {Computer Aided Verification (CAV) Tool Demo},
abstract = {
We describe a tool that applies theorem proving technology
to synthesize code fragments that use given library
functions. To determine candidate code fragments,
our approach takes into account polymorphic type
constraints as well as test cases. Our tool interactively displays a ranked
list of suggested code fragments that are appropriate for the current program point.
We have found our
system to be useful for synthesizing code fragments for
common programming tasks, and we believe it is a good platform
for exploring software synthesis techniques.
},
year = 2011}
@InProceedings{SuterETAL11SetswithCardinalityConstraintsin,
author = {Philippe Suter and Robin Steiger and Viktor Kuncak},
title = {Sets with Cardinality Constraints in Satisfiability Modulo Theories},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
year = 2011,
abstract = { Boolean Algebra with Presburger Arithmetic (BAPA) is a
decidable logic that can express constraints on sets of
elements and their cardinalities. Problems from
verification of complex properties of software
often contain fragments that belong to
quantifier-free BAPA (QFBAPA).
In contrast to many other NP-complete problems (such
as quantifier-free first-order logic or linear arithmetic),
the applications of QFBAPA to a broader set of problems has
so far been hindered by the lack of an efficient
implementation that can be used alongside other efficient
decision procedures.
We overcome these limitations by extending the efficient
SMT solver Z3 with the ability to reason about cardinality (QFBAPA)
constraints. Our implementation uses the DPLL(T) mechanism
of Z3 to reason about the top-level propositional
structure of a QFBAPA formula, improving the efficiency
compared to previous implementations. Moreover, we
present a new algorithm for automatically decomposing
QFBAPA formulas. Our algorithm alleviates the exponential
explosion of considering all Venn regions, significantly
improving the tractability of formulas with many set
variables. Because it is implemented as a theory plugin,
our implementation enables Z3 to prove formulas that use
QFBAPA constructs with constructs from other theories
that Z3 supports,
as well as with quantifiers. We have applied our
implementation to the verification of functional programs; we
show it can automatically prove formulas that no automated
approach was reported to be able to prove before. }
}
@InProceedings{JacobsKuncak11TowardsCompleteReasoningaboutAxiomaticSpecifications,
author = {Swen Jacobs and Viktor Kuncak},
title = {Towards Complete Reasoning about Axiomatic Specifications},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
year = 2011,
abstract = { To support verification of expressive properties of
functional programs, we consider algebraic style
specifications that may relate multiple user-defined
functions, and compare multiple invocations of a function
for different arguments.
We present decision procedures for reasoning about such universally quantified
properties of functional programs, using local
theory extension methodology. We establish new classes of
universally quantified formulas whose satisfiability can
be checked in a complete way by finite quantifier
instantiation. These classes include single-invocation
axioms that generalize standard function contracts, but
also certain many-invocation axioms, specifying that
functions satisfy congruence, injectivity, or monotonicity
with respect to abstraction functions, as well as conjunctions
of some of these properties. These many-invocation
axioms can specify correctness of abstract data type
implementations as well as certain information-flow
properties. We also present a decidability-preserving construction that enables
the same function to be specified using different classes
of decidable specifications on different partitions of its
domain. }
}
@TechReport{SuterETAL10OnSatisfiabilityModuloComputableFunctions,
author = {Philippe Suter and Ali Sinan K\"oksal and Viktor Kuncak},
title = {On Satisfiability Modulo Computable Functions},
institution = {EPFL},
number = {EPFL-REPORT},
year = 2010}
@TechReport{DarulovaKuncak10OnRigorousNumericalComputationasScalaLibrary,
author = {Eva Darulova and Viktor Kuncak},
title = {On Rigorous Numerical Computation as a Scala Library},
institution = {EPFL},
year = 2010,
number = {EPFL-REPORT-158754}}