-
Notifications
You must be signed in to change notification settings - Fork 9
/
pag.bib
1861 lines (1734 loc) · 91.1 KB
/
pag.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
% Program Analysis Group bibliography
% (Actually, only papers that do not include Michael Ernst as a coauthor.
% Blame either megalomania or a pre-existing directory organization that
% puts those files in ernst.bib.)
% This file (and ernst.bib) is processed by the bibtex2web program. See
% https://homes.cs.washington.edu/~mernst/software/bibtex2web.html
% for an explanation of the fields.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 1995
%%%
@Article{McCartneyGS1995,
author = "T. Paul McCartney and Kenneth J. Goldman and David E. Saff",
title = "EUPHORIA: End-user construction of direct manipulation
user interfaces for distributed applications",
journal = "Software Concepts and Tools",
year = 1995,
volume = 16,
number = 4,
pages = "147--159",
month = dec,
downloadsnonlocal =
"http://www.cs.wustl.edu/cs/playground/papers/wucs-95-29.ps PostScript",
abstract =
"The Programmers' Playground is a software library and run-time system for
creating distributed multimedia applications from collections of reusable
software modules. This paper presents the design and implementation of
EUPHORIA, Playground's user interface management system. Implemented as a
Playground module, EUPHORIA allows end-users to create direct manipulation
graphical user interfaces (GUIs) exclusively through the use of a graphics
editor. No programming is required. At run-time, attributes of the GUI
state can be exposed and connected to external Playground modules, allowing
the user to visualize and directly manipulate state information in remote
Playground modules. Features of EUPHORIA include real-time direct
manipulation graphics, constraint-based editing and visualization,
imaginary alignment objects, user-definable types, and user-definable
widgets with alternative representations.",
category = "Software engineering",
summary =
"EUPHORIA allows end-users to construct GUIs for distributed applications
using only a graphics editor, with no programming. Visual elements are
related to each other and the application state by constraints which can
be visualized and directly edited.",
nonPAG = 1,
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2001
%%%
@MastersThesis{Dean01,
author = "Laura Dean",
title = "Improved Simulation of {Input}/{Output} Automata",
school = MITEECS,
year = 2001,
address = MITaddr,
month = Sep,
basefilename = "ioa-simulator-dean-mengthesis",
abstract =
"The IOA Simulator is part of a collection of tools for developing and
analyzing distributed algorithms. This thesis describes several
improvements to the Simulator: adding new data type implementations,
sharing data types with the IOA Code Generator, improving the Simulator's
documentation, and adding an interface to Daikon, an invariant-discovery
tool. These improvements should increase the Simulator's usability as a
tool in writing and verifying algorithms for distributed systems.",
category = "Verification",
summary =
"The IOA language is used for modeling algorithms for distributed systems in
the Input-Output Automaton style. This thesis presents extensions to the
IOA Simulator, which is an interpreter for the IOA language. The extensions
make the Simulator more useful for testing and verification.",
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2002
%%%
@MastersThesis{Harder02:thesis,
author = "Michael Harder",
title = "Improving Test Suites via Generated Specifications",
school = MITEECS,
year = 2002,
address = MITaddr,
month = may,
supersededby = "Harder02:TR",
basefilename = "improve-testsuite-harder-mengthesis",
abstract =
"This thesis presents a specification-based technique for generating,
augmenting, and minimizing test suites. The technique is automatic
but assumes the existence of a test case generator. The technique
dynamically induces specifications from test suite executions. Test
suites can be generated by adding cases until the induced
specification stops changing. The resulting test suites have better
fault detection than suites of the same size with 100\% branch
coverage. Augmenting an existing test suite, such as a code-covering
suite, also increases its fault detection. Minimizing test suites
while holding the generated specification constant compares favorably
to previously-known techniques.
\par
These positive results can be explained by two insights, which the
thesis also justifies experimentally. First, given an a priori
specification (an oracle), the specification coverage of a test
suite compares the suite's induced specification with the oracle.
Experiments show that specification coverage is correlated with fault
detection, even when test suite size and code coverage are held
constant. Second, when tests are added at random to a suite,
specification coverage increases rapidly, then levels off at a high
value. Even without knowing the ideal specification that would be
induced by all possible tests, it is possible to produce a
specification very near that one.
\par
The thesis's test suite generation and augmentation technique increases
the specification coverage of the test suite, but without knowing the
oracle specification and without examining the code. In addition to
improving fault detection, the technique generates a specification
close to the oracle, which has many benefits in itself.",
category = "Testing",
summary =
"This thesis proposes a technique for selecting test cases that is
similar to structural code coverage techniques, but operates in the
semantic domain of program behavior rather than in the lexical domain
of program text. The technique outperforms branch coverage in test suite
size and in fault detection.",
usesDaikon = 1,
}
@TechReport{Harder02:TR,
author = "Michael Harder",
title = "Improving test suites via generated specifications",
institution = MITLCS,
year = 2002,
number = 848,
address = MITaddr,
month = jun # "~4,",
note = "Revision of author's Master's thesis",
supersededby = "HarderME03",
basefilename = "improve-testsuite-tr848",
abstract =
"This thesis presents a specification-based technique for generating,
augmenting, and minimizing test suites. The technique is automatic
but assumes the existence of a test case generator. The technique
dynamically induces specifications from test suite executions. Test
suites can be generated by adding cases until the induced
specification stops changing. The resulting test suites have better
fault detection than suites of the same size with 100\% branch
coverage. Augmenting an existing test suite, such as a code-covering
suite, also increases its fault detection. Minimizing test suites
while holding the generated specification constant compares favorably
to previously-known techniques.
\par
These positive results can be explained by two insights, which the
thesis also justifies experimentally. First, given an a priori
specification (an oracle), the specification coverage of a test
suite compares the suite's induced specification with the oracle.
Experiments show that specification coverage is correlated with fault
detection, even when test suite size and code coverage are held
constant. Second, when tests are added at random to a suite,
specification coverage increases rapidly, then levels off at a high
value. Even without knowing the ideal specification that would be
induced by all possible tests, it is possible to produce a
specification very near that one.
\par
The thesis's test suite generation and augmentation technique increases
the specification coverage of the test suite, but without knowing the
oracle specification and without examining the code. In addition to
improving fault detection, the technique generates a specification
close to the oracle, which has many benefits in itself.",
category = "Testing",
summary =
"This thesis proposes a technique for selecting test cases that is
similar to structural code coverage techniques, but operates in the
semantic domain of program behavior rather than in the lexical domain
of program text. The technique outperforms branch coverage in test suite
size and in fault detection.",
usesDaikon = 1,
}
@MastersThesis{Nimmer02:thesis,
author = "Jeremy W. Nimmer",
title = "Automatic Generation and Checking of Program Specifications",
school = MITEECS,
year = 2002,
address = MITaddr,
month = May,
supersededby = "Nimmer02:TR852 A revised version",
usesDaikon = 1,
}
@TechReport{Nimmer02:TR852,
author = "Jeremy W. Nimmer",
title = "Automatic Generation and Checking of Program Specifications",
institution = MITLCS,
year = 2002,
number = 852,
address = MITaddr,
month = jun # "~10,",
note = "Revision of author's Master's thesis",
supersededby = "NimmerE02:ISSTA A revised version,NimmerE02:FSE A revised version",
basefilename = "tr852",
abstract =
"This thesis introduces the idea of combining automatic generation and
checking of program specifications, assesses its efficacy, and suggests
directions for future research.
\par
Specifications are valuable in many aspects of program development,
including design, coding, verification, testing, and maintenance.
They also enhance programmers' understanding of code. Unfortunately,
written specifications are usually absent from programs, depriving
programmers and automated tools of their benefits.
\par
This thesis shows how specifications can be accurately recovered using
a two-stage system: propose likely specifications using a
dynamic invariant detector, and then confirm the likely specification
using a static checker. Their combination overcomes the weaknesses of
each: dynamically detected properties can provide goals for static
verification, and static verification can confirm properties proposed
by a dynamic~tool.
\par
Experimental results demonstrate that the dynamic component of
specification generation is accurate, even with limited test suites.
Furthermore, a user study indicates that imprecision during generation
is not a hindrance when evaluated with the help of a static checker.
We also suggest how to enhance the sensitivity of our system by
generating and checking context-sensitive properties.",
category = "Verification",
usesDaikon = 1,
}
@MastersThesis{Rolfe02,
author = "Alex Rolfe",
title = "Code Versioning in a Workflow Management System",
school = MITEECS,
year = 2002,
address = MITaddr,
month = May,
basefilename = "workflow-rolfe-mengthesis",
abstract =
"Workflow systems implement process definitions in laboratory, office, and
industrial settings. In many cases, the process definition is implicit in
the ad-hoc software written for a particular task. In other cases, a
generic framework provides basic functionality and structure, offering
quicker development and advanced features. Few workflow systems handle
changes in the process definition or the implementing code. This work
shows that complicated workflow processes can be composed of a few simple
primitives and that changes in the workflow structure and code can be
managed effectively.",
category = "Miscellaneous",
summary =
"Workflow systems permit high-level definition of code for managing some
physical process. This thesis proposes and implements a workflow system
that permits process definitions and implementing code to be changed, and
multiple versions of the process and code to be active simultaneously.",
}
@MastersThesis{Morse02,
author = "Benjamin Morse",
title = "A {C/C++} Front End for the {Daikon} Dynamic Invariant Detection System",
school = MITEECS,
year = 2002,
address = MITaddr,
month = aug,
basefilename = "cfrontend-morse-mengthesis",
abstract =
"The Daikon dynamic invariant detection suite is a system designed to
extract specifications from programs, in the form of information about
their variables and their relationships to each other. It does this by
instrumenting the source code of a target program, which inserts code
that directs the program to output the values of its variables and
other information when run. This data is then sent to Daikon proper,
which performs analysis on it and reports invariants about the program
variables. Daikon is a useful tool that can suggest invariants beyond
those provable by current static methods.
\par
While the invariant analysis tool is language independent, the front
ends --- tools that instrument of the user code --- must be written for
every language to be instrumented. There is a huge base of
pre-existing code written in C/C++ for which invariants can be
discovered. C/C++ are also widely deployed, comprise a large segment
of software currently in development, and are therefore valuable
candidates for analysis. The key difficulty in instrumenting a
type-unsafe language like C is that the instrumented program has to
determine what variables are valid, and to what extent, so that it does
not output garbage values or cause a segmentation fault by
dereferencing an invalid pointer. This thesis details the
implementation and performance of a Daikon front end for the C and C++
languages.",
category = "Static analysis",
summary =
"An instrumenter for data structures in C and C++ programs must determine
whether a given pointer is valid; whether it points to a single element or
an array; if an array, how large, and how much of it is in use. This
thesis solves these and related issues in C/C++ run-time instrumentation.",
}
@MastersThesis{Dodoo02:thesis,
author = "Nii Dodoo",
title = "Selecting Predicates for Conditional Invariant Detection Using Cluster Analysis",
school = MITEECS,
year = 2002,
address = MITaddr,
month = sep,
basefilename = "predicates-dodoo-mengthesis",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/predicates-dodoo-mengthesis.ps PostScript",
abstract =
"This thesis proposes a new technique for selecting predicates for
conditional program invariants --- that is, implications of the form
``p $\Rightarrow$ q'' whose consequent is true only when the predicate
is true. Conditional invariants are prevalent in recursive data
structures, which behave differently in the base and recursive cases,
and in many other situations.
\par
We argue that inferring conditional invariants in programs can be
reduced to the task of selecting suitable predicates from which to
infer these conditional invariants. It is computationally infeasible to
try every possible predicate for conditional properties, and therefore
it is necessary to limit possible predicates to only those likely to
give good results. This thesis describes the use of cluster analysis to
select suitable predicates for conditional invariant detection from
program execution traces. The primary thesis is: \emph{if ``natural''
clusters exist in the values of program execution traces, then
invariants over these clusters should serve as good predicates for
conditional invariant detection.}
\par
The conditional invariants inferred by cluster analysis can be useful
to programmers for a variety of tasks. In two experiments, we show that
they are useful in a static verification task and can help programmers
identify bugs in software programs, and we compare the results with
other methods for finding conditional invariants.",
category = "Static analysis",
summary =
"This thesis proposes the use of clustering, an artificial intelligence
technique, for splitting heterogeneous program analysis data into
homogeneous parts. The technique is effective in creating implications of
the form ``p => q'' that are useful in verification and bug detection.",
usesDaikon = 1,
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2003
%%%
@MastersThesis{NeWin2003,
author = "Toh {Ne Win}",
title = "Theorem-proving distributed algorithms with dynamic analysis",
school = MITEECS,
year = 2003,
address = MITaddr,
month = may,
basefilename = "thmprove-newin-mengthesis",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/thmprove-newin-mengthesis.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/thmprove-newin-mengthesis.ps PostScript",
abstract =
"Theorem provers are notoriously hard to use because of the amount of human
interaction they require, but they are important tools that can verify
infinite state distributed systems. We present a method to make
theorem-proving safety properties of distributed algorithms more productive
by reducing human intervention. We model the algorithms as I/O automata,
render the automata executable, and analyze the test executions with
dynamic invariant detection. The human work in using a theorem prover is
reduced because our technique provides two forms of assistance: lemmas
generated by the dynamic invariant detection for use in the prover; and
prover scripts, or tactics, generated from our experience with the I/O
automaton model and the knowledge embedded in the test suite used for
execution. We test our technique on three case studies: the Peterson
2-process mutual exclusion algorithm, a strong caching implementation of
shared memory, and Lamport's Paxos algorithm for distributed consensus.
\par
In the development and implementation of our method, we also improved the
tools for formal verification of I/O automata and for dynamic invariant
detection. We describe a new model for specifying I/O automata in the
Isabelle theorem prover's logic, and prove the soundness of a technique for
verifying invariants in this model in the Isabelle prover. We develop
methods for generating proofs of I/O automata for two theorem provers, the
Larch Prover and Isabelle/HOL. We show methods for executing I/O automata
for testing, by allowing the execution of some automata defined with
universal and existential quantifiers that were previously
non-executable. Lastly, we present improvements to dynamic invariant
detection in order to make it more scalable | in particular, we show how to
achieve efficient incremental dynamic invariant detection, where the
detection tool is only allowed to make one pass over its input executions.",
category = "Verification",
summary =
"This thesis proposes a new methodology, based on dynamic analysis, for
making theorem-provers easier to use. The dynamic analysis proposes both
lemmas that are necessary for a proof, and proof tactics that can be used
to prove the lemmas. Case studies with three distributed algorithms and
two theorem-provers show the technique to be effective.",
usesDaikon = 1,
}
@MastersThesis{Birka2003:thesis,
author = "Adrian Birka",
title = "Compiler-enforced immutability for the {Java} language",
school = MITEECS,
year = 2003,
address = MITaddr,
month = may,
supersededby = "Birka2003:TR",
abstract =
"This thesis presents the design, implementation, and evaluation of an
extension to the Java language, ConstJava, that is capable of expressing
immutability constraints and verifying them at compile time. The
specific constraint expressed in ConstJava is that the transitive state of
the object to which a given reference refers cannot be modified using
that reference.
\par
In addition to the ability to specify and enforce this basic
constraint, ConstJava includes several other features, such as mutable
fields, immutable classes, templates, and the const\_cast operator,
that make ConstJava a more useful language.
\par
The thesis evaluates the utility of ConstJava via experiments involving
writing ConstJava code and converting Java code to ConstJava code. The
evaluation of ConstJava shows that the language provides tangible
benefits in early detection and correction of bugs that would
otherwise be difficult to catch. There are also costs associated with
the use of ConstJava. These are minimized by ConstJava's backward
compatibility with Java, and by the high degree of inter-operability
of the two languages, which allows for a less painful transition from
Java to ConstJava.",
category = "Programming language design",
summary =
"This thesis presents a language (ConstJava), type system, implementation,
and evaluation of a safe mechanism for enforcing reference immutability,
where an immutable pointer may not be used to cause side effects to any
object reachable from it.",
}
@TechReport{Birka2003:TR,
author = "Adrian Birka",
title = "Compiler-enforced immutability for the {Java} language",
institution = MITLCS,
year = 2003,
number = "MIT-LCS-TR-908",
address = MITaddr,
month = jun,
note = "Revision of Master's thesis",
supersededby = "BirkaE2004",
abstract =
"This thesis presents the design, implementation, and evaluation of an
extension to the Java language, ConstJava, that is capable of expressing
immutability constraints and verifying them at compile time. The
specific constraint expressed in ConstJava is that the transitive state of
the object to which a given reference refers cannot be modified using
that reference.
\par
In addition to the ability to specify and enforce this basic
constraint, ConstJava includes several other features, such as mutable
fields, immutable classes, templates, and the const\_cast operator,
that make ConstJava a more useful language.
\par
The thesis evaluates the utility of ConstJava via experiments involving
writing ConstJava code and converting Java code to ConstJava code. The
evaluation of ConstJava shows that the language provides tangible
benefits in early detection and correction of bugs that would
otherwise be difficult to catch. There are also costs associated with
the use of ConstJava. These are minimized by ConstJava's backward
compatibility with Java, and by the high degree of inter-operability
of the two languages, which allows for a less painful transition from
Java to ConstJava.
\par
This technical report is a revision of the author's Master's thesis,
which was advised by Prof.~Michael D.~Ernst.",
basefilename = "immutability-tr908",
category = "Programming language design",
summary =
"This thesis presents a language (ConstJava), type system, implementation,
and evaluation of a safe mechanism for enforcing reference immutability,
where an immutable pointer may not be used to cause side effects to any
object reachable from it.",
}
@MastersThesis{Brun2003,
author = "Yuriy Brun",
title = "Software Fault Identification via Dynamic Analysis and
Machine Learning",
school = MITEECS,
year = 2003,
address = MITaddr,
month = aug # "~16,",
abstract =
"I propose a technique that identifies program properties that may
indicate errors. The technique generates machine learning models of
run-time program properties known to expose faults, and applies these
models to program properties of user-written code to classify and rank
properties that may lead the user to errors.
\par
I evaluate an implementation of the technique, the Fault Invariant
Classifier, that demonstrates the efficacy of the error finding
technique. The implementation uses dynamic invariant detection to
generate program properties. It uses support vector machine and
decision tree learning tools to classify those properties. Given a
set of properties produced by the program analysis, some of which are
indicative of errors, the technique selects a subset of properties
that are most likely to reveal an error. The experimental evaluation
over 941,000 lines of code, showed that a user must examine only the
2.2 highest-ranked properties for C programs and 1.7 for Java programs
to find a fault-revealing property. The technique increases the
relevance (the concentration of properties that reveal errors) by a
factor of 50 on average for C programs, and 4.8 for Java programs.",
supersededby = "BrunE2004",
basefilename = "faultid-brun-mengthesis",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/faultid-brun-mengthesis.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/faultid-brun-mengthesis.ps PostScript",
category = "Dynamic analysis",
summary =
"This thesis shows the efficacy of a technique that performs machine
learning over correct and incorrect programs, then uses the resulting
models to identify latent errors in other programs.",
usesDaikon = 1,
}
@InProceedings{PaluskaSYC2003,
author = "Justin Mazzola Paluska and David Saff and Tom Yeh and Kathryn Chen",
title = "Footloose: A Case for Physical Eventual Consistency and Selective Conflict Resolution",
crossref = "WMCSA2003",
pages = "170--180",
abstract =
"Users are increasingly inundated with small devices with communication
and storage capabilities. Unfortunately, the user is still responsible
for reconciling all of the devices whenever a change is made. We
present Footloose, a user-centered data store that can share data and
reconcile conflicts across diverse devices. Footloose is an optimistic
system based on physical eventual consistency{\,---\,}consistency based
on the movement of devices{\,---\,}and selective conflict
resolution{\,---\,}which allows conflicts to flow through devices that
cannot resolve the conflict to devices that can. Using these
techniques, Footloose can present consistent views of data on the
devices closest to the user without user interaction.",
category = "Miscellaneous",
basefilename = "footloose-wmcsa2003",
downloadsnonlocal =
"http://www.mit.edu/~jmp/research/footloose-wmcsa.pdf PDF;
http://www.mit.edu/~jmp/research/footloose-wmcsa.ps PostScript;
http://www.mit.edu/~jmp/research/footloose-wmcsa-presentation.pdf Presentation (PDF)",
summary =
"Footloose is a user-centered distributed data store that optimistically
shares data and reconciles conflicts across diverse, occasionally-connected
devices."
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2004
%%%
@MastersThesis{McCamant2004,
author = "Stephen McCamant",
title = "Predicting problems caused by component upgrades",
school = MITEECS,
year = 2004,
address = MITaddr,
month = jan # "~15,",
abstract =
"This thesis presents a new, automatic technique to assess whether
replacing a component of a software system by a purportedly compatible
component may change the behavior of the system.
The technique operates before integrating the new component into the
system or running system tests, permitting quicker and cheaper
identification of problems.
It takes into account the system's use of the component, because a
particular component upgrade may be desirable in one context but
undesirable in another.
No formal specifications are required, permitting detection of
problems due either to errors in the component or to errors in the
system.
Both external and internal behaviors can be compared, enabling
detection of problems that are not immediately reflected in the
output.
\par
The technique generates an operational abstraction for the old
component in the context of the system, and one for the new component
in the context of its test suite.
An operational abstraction is a set of program properties that
generalizes over observed run-time behavior.
Modeling a system as divided into modules, and taking into account the
control and data flow between the modules, we formulate a logical
condition to guarantee that the system's behavior is preserved across
a component replacement.
If automated logical comparison indicates that the new component does
not make all the guarantees that the old one did, then the upgrade may
affect system behavior and should not be performed without further
scrutiny.
\par
We describe a practical implementation of the technique, incorporating
enhancements to handle non-local state, non-determinism, and missing
test suites, and to distinguish old from new incompatibilities.
We evaluate the implementation in case studies using real-world
systems, including the Linux C library and 48 Unix programs.
Our implementation identified real incompatibilities among versions of
the C library that affected some of the programs, and it approved the
upgrades for other programs that were unaffected by the changes.",
basefilename = "upgrades-mccamant-smthesis",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/upgrades-mccamant-smthesis.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/upgrades-mccamant-smthesis.ps PostScript",
category = "Dynamic analysis",
summary =
"A software upgrade may break a customer's system because of differences
between it and the vendor's test environment. This thesis shows how to
predict such problems without having to integrate and test.",
usesDaikon = 1,
supersededby = "McCamant2004:ThesisTR"
}
@MastersThesis{Saff2004,
author = "David Saff",
title = "Automated continuous testing to speed software development",
school = MITEECS,
year = 2004,
address = MITaddr,
month = feb # "~3,",
abstract =
"Continuous testing is a new feature for software development
environments that uses excess cycles on a developer's workstation to
continuously run regression tests in the background, providing rapid
feedback about test failures as source code is edited. It is intended
to reduce the time and energy required to keep code well-tested and
prevent regression errors from persisting uncaught for long periods of
time. The longer that regression errors are allowed to
linger during development, the more time is wasted debugging and
fixing them once they are discovered.
\par
By monitoring and measuring software projects, we estimate that the
{\em wasted time}, consisting of this preventable extra fixing cost
added to the time spent running tests and waiting for them to
complete, account for 10--15\% of total development time. We present
a model of developer behavior that infers developer beliefs from
developer behavior and predicts behavior in new
environments{\,---\,}in particular, when changing testing
methodologies or tools to reduce wasted time. This model predicts
that continuous testing would reduce wasted time by 92--98\%, a
substantial improvement over other evaluated approaches such as automatic
test prioritization and changing manual test frequencies.
\par
A controlled human experiment indicates that continuous testing has a
statistically significant effect on developer success in completing a
programming task, without affecting time worked. Student developers
using continuous testing were three times more likely to complete a
task before the deadline than those without. Most participants found
continuous testing to be useful and believed that it helped them write
better code faster, and 90\% would recommend the tool to others.
\par
Continuous testing has been integrated into Emacs and Eclipse. We
detail the functional and technical design of the Eclipse plug-in,
which is now publicly released as a beta.",
category = "Testing",
supersededby = "SaffE2003 An extended version",
basefilename = "conttest-saff-smthesis",
summary =
"This thesis introduces the notion of continuous testing during development
and evaluates it via two experiments: one that observes a developer not
using continuous testing, and a controlled experiment on college students.",
}
@InProceedings{TipKB2003,
author = "Frank Tip and Adam Kie{\.z}un and Dirk B{\"a}umer",
authorASCII = "Adam Kiezun Dirk Baumer",
title = "Refactoring for generalization using type constraints",
crossref = "OOPSLA2003",
pages = "13--26",
abstract =
"Refactoring is the process of applying behavior-preserving transformations
(called ``refactorings'') in order to improve a program's design. Associated
with a refactoring is a set of preconditions that must be satisfied to
guarantee that program behavior is preserved, and a set of source code
modifications. An important category of refactorings is concerned with
generalization (e.g., Extract Interface for re-routing the access to a
class via a newly created interface, and Pull Up Members for moving members
into a superclass). For these refactorings, both the preconditions and the
set of allowable source code modifications depend on interprocedural
relationships between types of variables. We present an approach in which
type constraints are used to verify the preconditions and to determine the
allowable source code modifications for a number of generalization-related
refactorings. This work is implemented in the standard distribution of
Eclipse (see www.eclipse.org).",
category = "Software engineering",
basefilename = "refactoring-tip-ecoop2003",
summary =
"This paper describes the theoretical underpinnings behind two refactorings:
Extract Interface and Pull Up Members. The technical mechanism is to use
type constraints to determine which such changes are permitted.",
}
@TechReport{TipFDK2004,
author = "Frank Tip and Robert Fuhrer and Julian Dolby and Adam Kie{\.z}un",
authorASCII = "Adam Kiezun",
title = "Refactoring techniques for migrating applications to
generic {Java} container classes",
institution = "IBM T.J. Watson Research Center",
year = 2004,
type = "IBM Research Report",
number = "RC 23238",
address = "Yorktown Heights, NY, USA",
month = jun # "~2,",
abstract =
"Version 1.5 of the Java programming language will include generics, a
language construct for associating type parameters with classes and
methods. Generics are particularly useful for creating statically
type-safe, reusable container classes such that a store of an inappropriate
type causes a compile-time error, and that no down-casting is needed when
retrieving elements. The standard libraries released with Java 1.5 will
include generic versions of popular container classes such as HashMap and
ArrayList. This paper presents a method for refactoring Java programs that
use current container classes into equivalent Java 1.5 programs that use
their new generic counterparts. Our method uses a variation on an existing
model of type constraints to infer the element types of container objects,
and it is parameterized by how much, if any, context sensitivity to exploit
when generating these type constraints. We present both a
context-insensitive instantiation of the framework and one using a low-cost
variation on Agesen's Cartesian Product Algorithm. The method has been
implemented in Eclipse, a popular open-source development environment for
Java. We evaluated our approach on several small benchmark programs, and
found that, in all but one case, between 40\% and 100\% of all casts can be
removed.",
category = "Static analysis",
supersededby = "FuhrerTKDK2005",
basefilename = "refactoring-tip-rc23238",
summary =
"This paper gives a type-constraint-based method for converting non-generic
uses of Java collections into generic ones. In its context-sensitive
version it can also generify methods. It is implemented in Eclipse.",
}
@MastersThesis{Lin2004,
author = "Lee Lin",
title = "Improving adaptability via program steering",
school = MITEECS,
year = 2004,
address = MITaddr,
month = aug # "~12,",
abstract =
"A multi-mode software system contains several distinct modes of
operation and a controller for deciding when to switch between modes.
Even when developers rigorously test a multi-mode system before
deployment, they cannot foresee and test for every possible usage
scenario. As a result, unexpected situations in which the program
fails or underperforms (for example, by choosing a non-optimal mode)
may arise. This research aims to mitigate such problems by training
programs to select more appropriate modes during new situations. The
technique, called program steering, creates a new mode selector by
learning and extrapolating from previously successful experiences.
Such a strategy, which generalizes the knowledge that a programmer has
built into the system, may select an appropriate mode even when the
original programmer had not considered the scenario. We applied the
technique on simulated fish programs from MIT's Embodied Intelligence
class and on robot control programs written in a month-long
programming competition. The experiments show that the technique is
domain independent and that augmenting programs via program steering
can have a substantial positive effect on their performance in new
environments.",
supersededby = "LinE2004",
basefilename = "steering-lin-mengthesis",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/steering-lin-mengthesis.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/steering-lin-mengthesis.ps PostScript",
category = "Dynamic analysis",
summary =
"Program steering selects modalities for a program that may operate in
several modes. This thesis's experiments show that program steering can
substantially improve performance in unanticipated situations.",
usesDaikon = 1,
}
@MastersThesis{Donovan2004,
author = "Alan A. A. Donovan",
title = "Converting {Java} programs to use generic libraries",
school = MITEECS,
year = 2004,
address = MITaddr,
month = sep,
abstract =
"Java 1.5 will include a type system (called JSR-14) that supports
parametric polymorphism, or generic classes. This will bring many benefits
to Java programmers, not least because current Java practise makes heavy
use of logically-generic classes, including container classes. Translation
of Java source code into semantically equivalent JSR-14 source code
requires two steps: parameterisation (adding type parameters to class
definitions) and instantiation (adding the type arguments at each use of a
parameterised class). Parameterisation need be done only once for a class,
whereas instantiation must be performed for each client, of which there are
potentially many more. Therefore, this work focuses on the instantiation
problem. We present a technique to determine sound and precise JSR-14 types
at each use of a class for which a generic type specification is
available. Our approach uses a precise and context-sensitive pointer
analysis to determine possible types at allocation sites, and a
set-constraint-based analysis (that incorporates guarded, or conditional,
constraints) to choose consistent types for both allocation and declaration
sites. The technique safely handles all features of the JSR-14 type system,
notably the raw types (which provide backward compatibility) and
`unchecked' operations on them. We have implemented our analysis in a tool
that automatically inserts type arguments into Java code, and we report its
performance when applied to a number of real-world Java programs.",
basefilename = "generics-donovan-smthesis",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/generics-donovan-smthesis-2004.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/generics-donovan-smthesis-2004.ps PostScript",
supersededby = "DonovanKTE2004 An extended version",
category = "Static analysis",
summary =
"When type parameters are added to library code, client code should be
upgraded to supply parameters at each use of library classes. This
paper presents a sound and precise combined pointer and type-based
analysis that does so.",
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2005
%%%
@InProceedings{Saff2005,
author = "David Saff",
title = "Test factoring: Focusing test suites on the test at hand",
crossref = "ICSE2005",
pages = "",
NOabstract = "",
supersededby = "SaffE2004:mock-creation A summary",
basefilename = "test-factoring-doctoral-icse2005",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/test-factoring-doctoral-icse2005.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/test-factoring-doctoral-icse2005.ps PostScript",
category = "Testing",
summary =
"This one-page doctoral symposium summary outlines the motivation behind
test factoring: automatically converting each slow-running system tests
into a collection of fast-running unit tests.",
}
@MastersThesis{Williams2005,
author = "Amy Lynne Williams",
title = "Static Detection of Deadlock for {Java} Libraries",
school = MITEECS,
year = 2005,
address = MITaddr,
month = may,
category = "Static analysis",
supersededby = "WilliamsTE2005 An extended version",
summary =
"This thesis gives a technique for determining whether any invocation of
a library can lead to deadlock in the client program; it can also be
extended to the closed-world (whole-program) case.",
}
@InProceedings{FuhrerTKDK2005,
author = "Robert Fuhrer and Frank Tip and Adam Kie{\.z}un and
Julian Dolby and Markus Keller",
authorASCII = "Adam Kiezun",
title = "Efficiently refactoring {Java} applications to use generic
libraries",
crossref = "ECOOP2005",
pages = "71--96",
abstract =
"Java~1.5 generics enable the creation of reusable container classes with
compiler-enforced type-safe usage. This eliminates the need for potentially
unsafe down-casts when retrieving elements from containers. We present a
refactoring that replaces raw references to generic library classes with
parameterized references. The refactoring infers actual type parameters for
allocation sites and declarations using an existing framework of type
constraints, and removes casts that have been rendered redundant. The
refactoring was implemented in Eclipse, a popular open-source development
environment for Java, and laid the grounds for a similar refactoring in the
forthcoming Eclipse 3.1 release. We evaluated our work by refactoring
several Java programs that use the standard collections framework to use
Java 1.5's generic version instead. In these benchmarks, on average,
48.6\% of the casts are removed, and 91.2\% of the compiler warnings
related to the use of raw types are eliminated. Our approach distinguishes
itself from the state-of-the-art [8] by being more scalable, by its ability
to accommodate user-defined subtypes of generic library classes, and by
being incorporated in a popular integrated development environment.",
category = "Static analysis",
basefilename = "genericlibs-tip-ecoop2005",
summary =
"This paper gives a type-constraint-based method for converting non-generic
uses of Java collections into generic ones. In its context-sensitive
version it can also generify methods. It is implemented in Eclipse.",
}
@TechReport{McCamantM2005:TR,
author = "Stephen McCamant and Greg Morrisett",
title = "Efficient, verifiable binary sandboxing for a {CISC} architecture",
institution = MITCSAIL,
year = 2005,
number = {2005-030},
note = {(also MIT LCS TR \#988)},
address = MITaddr,
month = may,
abstract =
"Executing untrusted code while preserving security requires
enforcement of {\em memory} and {\em control-flow safety} policies:
untrusted code must be prevented from modifying memory or executing
code except as explicitly allowed.
Software-based fault isolation (SFI) or ``sandboxing'' enforces
those policies by rewriting the untrusted code at the level of
individual instructions.
However, the original sandboxing technique of Wahbe et al.\ is
applicable only to RISC architectures, and other previous work is
either insecure, or has been not described in enough detail to give
confidence in its security properties.
We present a novel technique that allows sandboxing to be easily
applied to a CISC architecture like the IA-32.
The technique can be verified to have been applied at load time, so
that neither the rewriting tool nor the compiler needs to be
trusted.
We describe a prototype implementation which provides a robust
security guarantee, is scalable to programs of any size, and has
low runtime overheads.
Further, we give a machine-checked proof that any program approved
by the verification algorithm is guaranteed to respect the desired
safety property.",
supersededby = "McCamantM2006",
NOTbasefilename = "pittsfield-tr988",
downloadsnonlocal =
"https://groups.csail.mit.edu/pag/pubs/pittsfield-tr988.pdf PDF;
https://groups.csail.mit.edu/pag/pubs/pittsfield-tr988.ps PostScript;
http://hdl.handle.net/1721.1/30542 DSpace",
category = "Security",
summary =
"This report describes an instruction-level rewriting technique to
enforce memory and control-flow safety. A prototype implementation
demonstrates the technique's scalability, and a machine-checked
proof formalizes its security guarantee.",
}
@MastersThesis{Pacheco2005,
author = "Carlos Pacheco",
title = "Eclat: Automatic generation and classification of test inputs",
school = MITEECS,
year = 2005,
address = MITaddr,
month = jun,
abstract =
"This thesis describes a technique that selects, from a large set of test
inputs, a small subset likely to reveal faults in the software under test.
The technique takes a program or software component, plus a set of correct
executions---say, from observations of the software running properly, or
from an existing test suite that a user wishes to enhance. The technique
first infers an operational model of the software's operation. Then,
inputs whose operational pattern of execution differs from the model in
specific ways are suggestive of faults. These inputs are further reduced
by selecting only one input per operational pattern. The result is a small
portion of the original inputs, deemed by the technique as most likely to
reveal faults. Thus, the technique can also be seen as an error-detection
technique.
\par
The thesis describes two additional techniques that complement test input
selection. One is a technique for automatically producing an oracle (a set
of assertions) for a test input from the operational model, thus
transforming the test input into a test case. The other is a
classification-guided test input generation technique that also makes use
of operational models and patterns. When generating inputs, it filters out
code sequences that are unlikely to contribute to legal inputs, improving
the efficiency of its search for fault-revealing inputs.
\par
We have implemented these techniques in the Eclat tool, which generates
unit tests for Java classes. Eclat's input is a set of classes to test and
an example program execution---say, a passing test suite. Eclat's output is
a set of JUnit test cases, each containing a potentially fault-revealing
input and a set of assertions at least one of which fails. In our
experiments, Eclat successfully generated inputs that exposed
fault-revealing behavior; we have used Eclat to reveal real errors in
programs. The inputs it selects as fault-revealing are an order of
magnitude as likely to reveal a fault as all generated inputs.",
supersededby = "PachecoE2005 An extended version",