-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathstups.bib
4269 lines (3930 loc) · 297 KB
/
stups.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
@INPROCEEDINGS{Le95_91,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {LOPSTR},
ISBN = {3-540-58792-6},
PAGES = {122--137},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {91},
STUPSREV = {Plagge},
TITLE = {Partial Evaluation of the "Real Thing"},
VOLUME = {883},
YEAR = {1994},
}
@INPROCEEDINGS{LeDe95_92,
AUTHOR = {Michael Leuschel and Danny De Schreye},
BOOKTITLE = {PEPM},
PAGES = {253--263},
PUBLISHER = {ACM Press},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/metaic.pdf},
STUPSOLD = {92},
STUPSREV = {Plagge},
TITLE = {Towards Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters},
YEAR = {1995},
}
@INPROCEEDINGS{LeDeMa95_93,
AUTHOR = {Michael Leuschel and Danny De Schreye and Bern Martens},
BOOKTITLE = {ILPS},
PAGES = {615--616},
PUBLISHER = {MIT Press},
STUPSOLD = {93},
STUPSREV = {Plagge},
TITLE = {Tutorial on Program Specialisation (abstract)},
YEAR = {1995},
}
@INPROCEEDINGS{LeMa95_94,
AUTHOR = {Michael Leuschel and Bern Martens},
BOOKTITLE = {Proc. Joint Workshop on Deductive Databases and Logic Programming and Abduction in Deductive Databases and Knowledge Based Systems},
PAGES = {81--95},
PUBLISHER = {GMD-Studien Nr. 266},
STUPSOLD = {94},
STUPSREV = {Plagge},
TITLE = {Obtaining Specialised Update Procedures through Partial Deduction of the Ground Representation},
YEAR = {1995},
}
@INPROCEEDINGS{LeMa95_95,
AUTHOR = {Michael Leuschel and Bern Martens},
BOOKTITLE = {ILPS},
PAGES = {495--509},
PUBLISHER = {MIT Press},
STUPSOLD = {95},
STUPSREV = {Plagge},
TITLE = {Partial Deduction of the Ground Representation and its Application to Integrity Checking},
YEAR = {1995},
}
@INPROCEEDINGS{JoLe96_82,
AUTHOR = {Jesper J{ø}rgensen and Michael Leuschel},
BOOKTITLE = {Dagstuhl Seminar on Partial Evaluation},
EDITOR = {O. Danvy and R. Glueck and P. Thiemann},
ISBN = {3-540-61580-6},
PAGES = {238--262},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/cogendag.pdf},
STUPSOLD = {82},
STUPSREV = {Plagge},
TITLE = {Efficiently Generating Efficient Generating Extensions in {Prolog}},
VOLUME = {1110},
YEAR = {1996},
}
@INPROCEEDINGS{JoLeMa96_84,
AUTHOR = {Jesper J{ø}rgensen and Michael Leuschel and Bern Martens},
BOOKTITLE = {LOPSTR},
EDITOR = {J. Gallagher},
ISBN = {3-540-62718-9},
MONTH = {August},
PAGES = {59--82},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/cppd.pdf},
STUPSOLD = {84},
STUPSREV = {Plagge},
TITLE = {Conjunctive Partial Deduction in Practice},
VOLUME = {1207},
YEAR = {1996},
}
@INPROCEEDINGS{Le96_85,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {Proc. Logic Databases and the Meaning of Change: Dagstuhl-Seminar-Report 157},
EDITOR = {J. Bocca and H. Decker and A. Voronkov},
PAGES = {18--19},
PUBLISHER = {IBFI GmbH, Schloss Dagstuhl},
STUPSOLD = {85},
STUPSREV = {Schneider},
TITLE = {Specialised Integrity Checking by Combining Conjunctive Partial Deduction and Abstract Interpretation},
YEAR = {1996},
}
@INPROCEEDINGS{LeDe96_86,
AUTHOR = {Michael Leuschel and Danny De Schreye},
BOOKTITLE = {Proceedings PLILP'96},
EDITOR = {H. Kuchen and S. D. Swierstra},
ISBN = {3-540-61756-6},
MONTH = {September},
PAGES = {137--151},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/msvplilp.pdf},
STUPSOLD = {86},
STUPSREV = {Plagge},
TITLE = {Logic Program Specialisation: How To Be More Specific},
VOLUME = {1140},
YEAR = {1996},
}
@INPROCEEDINGS{LeDe96_87,
AUTHOR = {Michael Leuschel and Danny De Schreye},
BOOKTITLE = {LOPSTR},
EDITOR = {J. Gallagher},
ISBN = {3-540-62718-9},
MONTH = {August},
PAGES = {58},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {87},
STUPSREV = {Plagge},
TITLE = {Logic Program Specialisation: How To Be More Specific (abstract)},
VOLUME = {1207},
YEAR = {1996},
}
@INPROCEEDINGS{LeDede96_88,
AUTHOR = {Michael Leuschel and Danny De Schreye and D. Andre de Waal},
BOOKTITLE = {JICSLP},
EDITOR = {M. Maher},
MONTH = {September},
PAGES = {319--332},
PUBLISHER = {MIT Press},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/fold.iclp.pdf},
STUPSOLD = {88},
STUPSREV = {Plagge},
TITLE = {A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration},
YEAR = {1996},
}
@INPROCEEDINGS{LeMa96_89,
AUTHOR = {Michael Leuschel and Bern Martens},
BOOKTITLE = {Dagstuhl Seminar on Partial Evaluation},
EDITOR = {O. Danvy and R. Glueck and P. Thiemann},
ISBN = {3-540-61580-6},
PAGES = {263--283},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/papdag.pdf},
STUPSOLD = {89},
STUPSREV = {Plagge},
TITLE = {Global Control for Partial Deduction through Characteristic Atoms and Global Trees},
VOLUME = {1110},
YEAR = {1996},
}
@INPROCEEDINGS{LeSo96_90,
AUTHOR = {Michael Leuschel and Morten Heine S{ø}rensen},
BOOKTITLE = {LOPSTR},
EDITOR = {J. Gallagher},
ISBN = {3-540-62718-9},
MONTH = {August},
PAGES = {83--103},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {90},
STUPSREV = {Plagge},
TITLE = {Redundant Argument Filtering of Logic Programs},
VOLUME = {1207},
YEAR = {1996},
}
@THESIS{Jastram_thesis_1997,
ABSTRACT = {<b>Localization</b> Localization is the process of determining the rigid-body translations and rotations that must be performed on a set of points measured on a manufactured surface (like a propeller blade) to move those points into the closest correspondence with the ideal design surface. An additional parameter is an offset distance, such that the Euclidean motion brings the measured points as close as possible to an offset of the design surface. An algorithm to determine the seven parameters (three rotations, three translations, one offset) was developed in 1991 by R. A. Jinkerson. But that algorithm makes some assumptions about the surface and the measured points, which are sometimes not fulfilled. Specifically, it assumes, that a measured point has always an orthogonal projection on the offset surface, regardless of the translation and rotation parameters. This thesis extends Jinkerson's algorithm, so that these assumptions are not necessary any longer. This involves the development of a new objective function and its gradient.<br><br> <b>Feature extraction</b> During the manufacturing process, a propeller blade surface is subject to manufacturing inaccuracies, that result in small changes to the data describing its features. It is therefore desirable to recompute these features for comparison with the original design data. Most of the characteristics of a propeller blade are embedded in the camber lines of its hydrofoil sections. The objective of this part of the thesis is to recompute the camber line from a hydrofoil shape curve. An algorithm for this task has already been developed, but it makes the assumption that the blade thickness has a single maximum, which is often not fulfilled, especially, if the hydrofoil has been generated from measured data. In this thesis, a new algorithm has been developed. It generates a highly accurate camber line by using a two pass iteration method: The first pass generates an approximation of the camber line, and the second pass refines this approximation to the desired accuracy.},
AUTHOR = {Michael Jastram},
INSTITUTION = {Massachusetts Institute of Technology},
MONTH = {December},
STUPSREV = {Jastram},
TITLE = {Inspection and Feature Extraction of Marine Propellers},
TYPE = {mathesis},
YEAR = {1996},
}
@ARTICLE{Le97_79,
AUTHOR = {Michael Leuschel},
JOURNALTITLE = {AI Communications},
NUMBER = {2},
PAGES = {127--128},
STUPSOLD = {79},
STUPSREV = {Plagge},
TITLE = {Advanced Techniques for Logic Program Specialisation},
VOLUME = {10},
YEAR = {1997},
}
@INPROCEEDINGS{Le97_80,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {ILPS},
MONTH = {Oct},
PAGES = {413--414},
PUBLISHER = {MIT Press},
STUPSOLD = {80},
STUPSREV = {Plagge},
TITLE = {Specialization of Declarative Programs and its Application (workshop overview)},
YEAR = {1997},
}
@INPROCEEDINGS{Le97_81,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming},
EDITOR = {German Puebla},
MONTH = {October},
SERIES = {Universidad Politécnica de Madrid Tech. Rep. CLIP7/97.1},
STUPSOLD = {81},
STUPSREV = {Plagge},
TITLE = {The {Ecce} Partial Deduction System},
YEAR = {1997},
}
@PROCEEDINGS{Leuschel:SP97,
EDITOR = {Michael Leuschel},
MONTH = {October},
PUBLISHER = {K. U. Leuven, Tech. Rep. CW 255, also as DIKU Report 97/30, University of Copenhagen},
STUPSOLD = {103},
STUPSREV = {Plagge},
TITLE = {Proceedings of the ILPS'97 Workshop on Specialisation of Declarative Programs and its Application},
YEAR = {1997},
}
@THESIS{Le97_216,
AUTHOR = {Michael Leuschel},
INSTITUTION = {K.U. Leuven},
MONTH = {May},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/phd.pdf},
STUPSOLD = {216},
STUPSREV = {Plagge},
TITLE = {Advanced Techniques for Logic Program Specialisation},
TYPE = {phdthesis},
YEAR = {1997},
}
@THESIS{Ha97_302,
ABSTRACT = {CSP-Z ist eine Sprache zur Spezifikation zustandsbasierter kommunizierender Systeme, welche die Prozeßalgebra CSP und die Z-Notation zusammenführt. Die Semantik von CSP-Z-Spezifikationen wird durch das Failures/Divergences-Modell von CSP beschrieben, das von Roscoe angepaßt wurde, um unbeschränkten Nichtdetermismus besser behandeln zu können. Für CSP gibt es eine Verfeinerungstheorie, die auf dem Failures/Divergences-Modell basiert. Diese Theorie lässt sich in einfacher Weise auf CSP-Z übertragen. Ziel dieser Arbeit ist es die existierende Verfeinerungstheorie von Z für CSP-Z nutzbar zu machen. Mit Z können Datentypen prädikativ beschrieben werden, die nicht oder nur mit großem Aufwand zu implementieren sind. Doch bieten diese Datentypen den Vorteil, daß sie zu leichter verständlichen Spezifikationen führen, da bei starker Abstraktion viele für die Funktionalität des zu entwickelnden Programms unwesentliche Details wegfallen. Zu einem späteren Zeitpunkt werden jedoch besser implementierbare Datentypen benötigt. Es ist in Z möglich, einen (abstrakten) Datentypen durch einen anderen (konkreten) Datentypen zu ersetzen, so daß Programme, die bei Verwendung des abstrakten Datentypen korrekt waren, es auch bei Verwendung des konkreten Datentypen bleiben. Dieses Verfahren heißt Datenverfeinerung. Als Beweismethode zum Nachweis einer Datenverfeinerung dient die Simulation. Bis zu einem gewissen Grade lässt sich die Datenverfeinerungstheorie auch im Zusammenhang mit unsichtbaren Operationen verwenden, die durch Hiding entstehen. Es werden einige Regeln entwickelt, die auf den Regeln zur Datenverfeinerung in Z basieren und benutzt werden können, um Simulationsbeziehungen zwischen CSP-Z-Spezifikationen zu beweisen. Die Anwendung der entwickelten Regeln wird anhand kleinerer Fallstudien veranschaulicht.},
AUTHOR = {Stefan Hallerstede},
INSTITUTION = {Carl von Ossietzky Universität Oldenburg},
MONTH = {Januar},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/diplom.pdf},
STUPSOLD = {302},
STUPSREV = {Hallerstede},
TITLE = {Semantische Fundierung von CSP-Z},
TYPE = {mathesis},
YEAR = {1997},
}
@INPROCEEDINGS{BrLeSa98_68,
AUTHOR = {Maurice Bruynooghe and Michael Leuschel and Konstantinos Sagonas},
BOOKTITLE = {ESOP},
EDITOR = {C. Hankin},
ISBN = {3-540-64302-8},
MONTH = {April},
PAGES = {27--41},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/bta.esop.pdf},
STUPSOLD = {68},
STUPSREV = {Plagge},
TITLE = {A Polyvariant Binding-Time Analysis for Off-line Partial Deduction},
VOLUME = {1381},
YEAR = {1998},
}
@INPROCEEDINGS{DeDeLeMaSa98_69,
AUTHOR = {Stefaan Decorte and Danny De Schreye and Michael Leuschel and Bern Martens and Konstantinos Sagonas},
BOOKTITLE = {LOPSTR '97},
EDITOR = {N. Fuchs},
ISBN = {3-540-65074-1},
MONTH = {July},
PAGES = {111--127},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/term.paper.pdf},
STUPSOLD = {69},
STUPSREV = {Plagge},
TITLE = {Termination Analysis for Tabled Logic Programming},
VOLUME = {1463},
YEAR = {1998},
}
@INPROCEEDINGS{Le98_70,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {LOPSTR '98},
EDITOR = {P. Flener},
ISBN = {3-540-65765-7},
MONTH = {June},
PAGES = {199--218},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/gh-lopstr.pdf},
STUPSOLD = {70},
STUPSREV = {Plagge},
TITLE = {Improving Homeomorphic Embedding for Online Termination},
VOLUME = {1559},
YEAR = {1998},
}
@INPROCEEDINGS{Le98_71,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {Proceedings SAS},
EDITOR = {Giorgio Levi},
ISBN = {3-540-65014-8},
MONTH = {September},
PAGES = {230--245},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/gh-sas.pdf},
STUPSOLD = {71},
STUPSREV = {Plagge},
TITLE = {On the Power of Homeomorphic Embedding for Online Termination},
VOLUME = {1503},
YEAR = {1998},
}
@INPROCEEDINGS{Le98_72,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {IJCSLP},
EDITOR = {J. Jaffar},
PAGES = {220--234},
PUBLISHER = {MIT Press},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/apd.jicslp98.pdf},
STUPSOLD = {72},
STUPSREV = {Plagge},
TITLE = {Program Specialisation and Abstract Interpretation Reconciled},
YEAR = {1998},
}
@ARTICLE{LeDe98_73,
AUTHOR = {Michael Leuschel and Danny De Schreye},
JOURNALTITLE = {New Generation Computing},
NUMBER = {3},
PAGES = {283--342},
STUPSOLD = {73},
STUPSREV = {Plagge},
TITLE = {Constrained Partial Deduction and the Preservation of Characteristic Trees},
VOLUME = {16},
YEAR = {1998},
}
@ARTICLE{LeDe98_74,
AUTHOR = {Michael Leuschel and Danny De Schreye},
JOURNALTITLE = {Journal of Logic Programming},
NUMBER = {2},
PAGES = {149--193},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/icjourn.ps},
STUPSOLD = {74},
STUPSREV = {Plagge},
TITLE = {Creating Specialised Integrity Checks Through Partial Evaluation of Meta-interpreters},
VOLUME = {36},
YEAR = {1998},
}
@ARTICLE{LeMaDe98_75,
AUTHOR = {Michael Leuschel and Bern Martens and Danny De Schreye},
JOURNALTITLE = {ACM Transactions on Programming Languages and Systems},
MONTH = {January},
NUMBER = {1},
PAGES = {208--258},
STUPSOLD = {75},
STUPSREV = {Plagge},
TITLE = {Controlling Generalisation and Polyvariance in Partial Deduction of Normal Logic Programs},
VOLUME = {20},
YEAR = {1998},
}
@ARTICLE{LeMaDe98_76,
AUTHOR = {Michael Leuschel and Bern Martens and Danny De Schreye},
JOURNALTITLE = {ACM Computing Surveys},
MONTH = {September},
NUMBER = {3es},
STUPSOLD = {76},
STUPSREV = {Plagge},
TITLE = {Some Achievements and Prospects in Partial Deduction},
VOLUME = {30},
YEAR = {1998},
}
@INPROCEEDINGS{LeMaSa98_77,
AUTHOR = {Michael Leuschel and Bern Martens and Konstantinos Sagonas},
BOOKTITLE = {LOPSTR '97},
EDITOR = {N. Fuchs},
ISBN = {3-540-65074-1},
MONTH = {July},
PAGES = {189--205},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/xsb.lopstr.pdf},
STUPSOLD = {77},
STUPSREV = {Plagge},
TITLE = {Preserving Termination of Tabled Logic Programs While Unfolding},
VOLUME = {1463},
YEAR = {1998},
}
@ARTICLE{SaLe98_78,
AUTHOR = {Konstantinos Sagonas and Michael Leuschel},
JOURNALTITLE = {ACM Computing Surveys},
MONTH = {September},
NUMBER = {3es},
STUPSOLD = {78},
STUPSREV = {Plagge},
TITLE = {Extending Partial Deduction to Tabled Execution: Some Results and Open Issues},
VOLUME = {30},
YEAR = {1998},
}
@ARTICLE{DeGlJoLeMaSo99_57,
AUTHOR = {Danny De Schreye and Robert Glueck and Jesper J{ø}rgensen and Michael Leuschel and Bern Martens and Morten H. S{ø}rensen},
JOURNALTITLE = {Journal of Logic Programming},
MONTH = {November},
NUMBER = {2--3},
PAGES = {231--277},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/jlpfold.pdf},
STUPSOLD = {57},
STUPSREV = {Plagge},
TITLE = {Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments},
VOLUME = {41},
YEAR = {1999},
}
@INPROCEEDINGS{GlLe99_58,
AUTHOR = {Robert Glueck and Michael Leuschel},
BOOKTITLE = {Ershov Memorial Conference},
ISBN = {3-540-67102-1},
PAGES = {93--100},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {58},
STUPSREV = {Plagge},
TITLE = {Abstraction-Based Partial Deduction for Solving Inverse Problems -- A Transformational Approach to Software Verification},
VOLUME = {1755},
YEAR = {1999},
}
@INPROCEEDINGS{HaBuCuHeLeMaSmUlWa99_59,
ABSTRACT = {An abstract model of an industrial distributed data base application has been studied using process based, state based, and queueing theory based methods. The methods supported by graphical notations and/or integrated development environments were found to be easiest to work with. The methods supported by model checkers were the most successful in obtaining relevant information about the application. Applying a number of different methods to study one particular model encourages a problem to be viewed from different angles. This gives complementary information about the model. We report on a variety of problems of the model found through various routes. Our main conclusion is that asking experts to apply different methods and tools at a sufficiently abstract level can be done effectively revealing a broad range of information about the considered application.},
AUTHOR = {P. Hartel and Michael Butler and Andrew Currie and P. Henderson and Michael Leuschel and A. Martin and A. Smith and Ulrich Ultes-Nitsche and R.J. Walters},
BOOKTITLE = {Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems},
EDITOR = {S. Gnesi and D. Latella},
ISBN = {88-7958-009-4},
MONTH = {July},
PAGES = {179--203},
PUBLISHER = {STAR/CNR, Pisa, Italy},
STUPSOLD = {59},
STUPSREV = {Plagge},
TITLE = {Questions and Answers About Ten Formal Methods},
YEAR = {1999},
}
@INPROCEEDINGS{Le99_60,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School},
ISBN = {3-540-66710-5},
PAGES = {271--292},
PUBLISHER = {Springer-Verlag},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/pesummer2.pdf},
STUPSOLD = {60},
STUPSREV = {Plagge},
TITLE = {Advanced Logic Program Specialisation},
YEAR = {1999},
}
@PROCEEDINGS{Le99_61,
EDITOR = {Michael Leuschel},
JOURNALTITLE = {Electronic Notes in Theoretical Computer Science},
MONTH = {December},
NUMBER = {2},
PAGES = {94--},
STUPSOLD = {61},
STUPSREV = {Plagge},
TITLE = {Int. Workshop on Optimization and Implementation of Declarative Programs},
VOLUME = {30},
YEAR = {1999},
}
@INPROCEEDINGS{Le99_62,
AUTHOR = {Michael Leuschel},
BOOKTITLE = {Partial Evaluation: Practice and Theory},
EDITOR = {John Hatcliff and Torben AE Mogensen and Peter Thiemann},
ISBN = {3-540-66710-5},
PAGES = {155--188},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/pesummer1.pdf},
STUPSOLD = {62},
STUPSREV = {Plagge},
TITLE = {Logic Program Specialisation},
VOLUME = {1706},
YEAR = {1999},
}
@ARTICLE{LeJo99_63,
AUTHOR = {Michael Leuschel and Jesper J{ø}rgensen},
JOURNALTITLE = {Electronic Notes in Theoretical Computer Science},
NUMBER = {2},
PAGES = {157-162},
STUPSOLD = {63},
STUPSREV = {Plagge},
TITLE = {Efficient Specialisation in {Prolog} Using the Hand-Written Compiler Generator {LOGEN}},
VOLUME = {30},
YEAR = {1999},
}
@REPORT{LeJo99_64,
AUTHOR = {Michael Leuschel and Jesper J{ø}rgensen},
INSTITUTION = {University of Southampton},
MONTH = {September},
NUMBER = {DSSE-TR-99-6},
STUPSOLD = {64},
STUPSREV = {Plagge},
TITLE = {Efficient Specialisation in {Prolog} Using a Hand-Written Compiler Generator},
TYPE = {techreport},
YEAR = {1999},
}
@INPROCEEDINGS{LeLiTh99_65,
AUTHOR = {Michael Leuschel and Nick Linnenbruegger and Jerome Thoma},
BOOKTITLE = {Proceedings of the Formal Grammar Conference FG'99},
EDITOR = {G-J. M. Kruijff and R. T. Oerle},
MONTH = {August},
PAGES = {93--101},
PUBLISHER = {University of Utrecht},
STUPSOLD = {65},
STUPSREV = {Plagge},
TITLE = {Analyzing Context-Free and Context-Sensitive Grammars by Abstract Interpretation},
YEAR = {1999},
}
@INPROCEEDINGS{LeMa99_66,
ABSTRACT = {We illustrate the use of logic programming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic program specialisation and analysis techniques. The power of the approach is illustrated on several examples. For that, the efficient tools logen and ecce are used. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.},
AUTHOR = {Michael Leuschel and Thierry Massart},
BOOKTITLE = {LOPSTR '99},
EDITOR = {A. Bossi},
ISBN = {3-540-67628-7},
MONTH = {September},
PAGES = {63--82},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/mc-lopstr99.pdf},
STUPSOLD = {66},
STUPSREV = {Plagge},
TITLE = {Infinite State Model Checking by Abstract Interpretation and Program Specialisation},
VOLUME = {1817},
YEAR = {1999},
}
@INPROCEEDINGS{MaLe99_67,
AUTHOR = {Jonathan C. Martin and Michael Leuschel},
BOOKTITLE = {Ershov Memorial Conference},
ISBN = {3-540-67102-1},
PAGES = {101--112},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {67},
STUPSREV = {Plagge},
TITLE = {Sonic Partial Deduction},
VOLUME = {1755},
YEAR = {1999},
}
@REPORT{HaBu99_300,
ABSTRACT = {Existing refinement frameworks such as B allow a developer to specify a system on an abstract level. Subsequently, this abstract specification is refined into an implementation that performs the specified task. In this paper a conventional refinement approach is extended with a means for performance analysis. This new approach guides a developer towards well-performing implementations throughout the refinement process. The main achievement of this work is an elaboration of a connection between performance and trace refinement.},
AUTHOR = {Stefan Hallerstede and Michael Butler},
DBSLINKS = {[http://eprints.ecs.soton.ac.uk/2949/|PDF]},
INSTITUTION = {Electronics and Computer Science, University of Southampton},
STUPSOLD = {300},
STUPSREV = {Hallerstede},
TITLE = {Refinement of Dynamic Systems},
TYPE = {techreport},
YEAR = {1999},
}
@INPROCEEDINGS{CuLeMa00_49,
ABSTRACT = {We show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between ``classical'' model checking and refinement checking.},
AUTHOR = {Andrew Currie and Michael Leuschel and Thierry Massart},
BOOKTITLE = {Proceedings VCL'2000},
LOCATION = {London, UK},
MONTH = {July},
STUPSOLD = {49},
STUPSREV = {leuschel},
TITLE = {{LTL} Model Checking of {CSP} by Refinement: How to Make {FDR} Spin},
YEAR = {2000},
}
@INPROCEEDINGS{LeLe00_50,
AUTHOR = {Helko Lehmann and Michael Leuschel},
BOOKTITLE = {Computational Logic},
EDITOR = {John LLoyd},
ISBN = {3-540-67797-6},
MONTH = {July},
PAGES = {762--776},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {50},
STUPSREV = {Plagge},
TITLE = {Decidability Results for the Propositional Fluent Calculus},
VOLUME = {1861},
YEAR = {2000},
}
@INPROCEEDINGS{LeLe00_51,
AUTHOR = {Helko Lehmann and Michael Leuschel},
BOOKTITLE = {LPAR},
EDITOR = {Michel Parigot and Andrei Voronkov},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/paper_camera_ready.ps},
STUPSOLD = {51},
STUPSREV = {Plagge},
TITLE = {Solving Planning Problems by Partial Deduction},
VOLUME = {1955},
YEAR = {2000},
}
@REPORT{LeBr00_52,
ABSTRACT = {Partial deduction is a source-to-source technique for specialising logic programs. This is (mostly) done by a well-automated application of parts of the Burstall and Darlington unfold/fold transformation framework. One of the main challenges of partial deduction is automatic control, which has to ensure correctness, efficiency, and termination. In this survey and tutorial, we present the essential developments over the past 10 years, and discuss their respective merits and shortcomings. We also present the current state of the art and discuss areas where further research is needed to enable more widespread practical use of partial deduction and realise its potential as a tool for systematic program development.},
AUTHOR = {Michael Leuschel and Maurice Bruynooghe},
INSTITUTION = {University of Southampton},
MONTH = {October},
PAGES = {45--},
STUPSOLD = {52},
STUPSREV = {Plagge},
TITLE = {Control Issues in Partial Deduction: The Ever Ending Story},
TYPE = {techreport},
YEAR = {2000},
}
@INPROCEEDINGS{LeLe00_53,
ABSTRACT = {In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that partial deduction is powerful enough to mimic certain algorithms to decide coverability properties of Petri nets. These algorithms are forward algorithms and hard to scale up to deal with more complicated systems. Recently, it has been proposed to use a backward algorithm scheme instead. This scheme is applicable to so--called well--structured transition systems and was successfully used, e.g., to solve coverability problems for reset Petri nets. In this paper, we discuss how partial deduction can mimic many of these backward algorithms as well. We prove this link in particular for reset Petri nets and Petri nets with transfer and doubling arcs. We thus establish a surprising link between algorithms in Petri net theory and program specialisation, and also shed light on the power of using logic program specialisation for infinite state model checking.},
AUTHOR = {Michael Leuschel and Helko Lehmann},
BOOKTITLE = {Computational Logic},
EDITOR = {John Lloyd and Verónica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Luı́s Moniz Pereira and Yehoshua Sagiv and Peter J. Stuckey},
ISBN = {3-540-67797-6},
MONTH = {July},
PAGES = {101--115},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/CL2000_camera_ready.pdf},
STUPSOLD = {53},
STUPSREV = {Plagge},
TITLE = {Coverability of Reset Petri Nets and other Well-Structured Transition Systems by Partial Deduction},
VOLUME = {1861},
YEAR = {2000},
}
@INPROCEEDINGS{LeLe00_54,
ABSTRACT = {In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one particular class of problem--coverability for (infinite state) Petri nets--and shows how existing techniques and tools for declarative programs can be successfully applied. In particular, we show that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri Nets. We also prove that two particular instances of partial deduction exactly compute the Karp-Miller tree as well as Finkel's minimal coverability set. We thus establish an interesting link between algorithms for Petri nets and logic program specialisation.},
AUTHOR = {Michael Leuschel and Helko Lehmann},
BOOKTITLE = {PPDP},
EDITOR = {Maurizio Gabbrielli and Frank Pfenning},
MONTH = {September},
PAGES = {268--279},
PUBLISHER = {ACM Press},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/PPDP2000.pdf},
STUPSOLD = {54},
STUPSREV = {Plagge},
TITLE = {Solving Coverability Problems of Petri Nets by Partial Deduction},
YEAR = {2000},
}
@PROCEEDINGS{PoRaUl00_55,
ABSTRACT = {The aim of this workshop is to bring together researchers working on the interplay between verification techniques (e.g., model checking, reduction, and abstraction) and logic programming techniques (e.g., constraints, abstract interpretation, program transformation).},
DBSLINKS = {[http://users.ecs.soton.ac.uk/mal/vcl2000.html|VCL'2000 Website]},
EDITOR = {Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche},
MONTH = {July},
PAGES = {150--},
STUPSOLD = {55},
STUPSREV = {leuschel},
TITLE = {Proceedings of the Workshop on Verification and Computational Logic VCL'2000},
YEAR = {2000},
}
@INPROCEEDINGS{AdLe01_42,
ABSTRACT = {In recent years, methods for analyzing and parallelizing sequential code using data analysis and loop transformations have been developed. These techniques have proved remarkably successful, and have been used to move from sequential to parallel codes, or to improve efficiency of existing parallel codes. Our research focuses on Fortran code optimisation for parallelisation in Shared Memory architectures by using data analysis and loop source-to-source transformations. Our optimisation strategy, although designed for OpenMP directives, is sufficiently general to be used for pure Fortran code. Our algorithm has been implemented as a tool called Automatic Guidance Module (AGM), and have received high evaluation scores from our industrial partners},
AUTHOR = {Laksono Adhianto and Michael Leuschel},
BOOKTITLE = {Proceedings of ISSM},
MONTH = {August},
STUPSOLD = {42},
STUPSREV = {Plagge},
TITLE = {Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism},
YEAR = {2001},
}
@ARTICLE{GlHaLeMa01_43,
AUTHOR = {Hugh Glaser and Pieter H. Hartel and Michael Leuschel and Andrew Martin},
EDITOR = {Allen Kent and James G Williams},
ISBN = {0-8247-2726-6},
JOURNALTITLE = {Encyclopaedia of Microcomputers},
PAGES = {79--102},
PUBLISHER = {Marcel Dekker Inc},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/dsse-tr-2000-1.ps},
STUPSOLD = {43},
STUPSREV = {Plagge},
TITLE = {Declarative Languages in Education},
VOLUME = {27},
YEAR = {2001},
}
@INPROCEEDINGS{Le01_44,
ABSTRACT = {We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing, prototyping, animating new specification languages. In particular, we present the new high-level specification language CSP(LP), unifying CSP with concurrent (constraint) logic programming, and which can be used to formally reason both about logical and concurrent aspects of critical systems.},
AUTHOR = {Michael Leuschel},
BOOKTITLE = {PADL},
ISBN = {3-540-41768-0},
ISSN = {0302-9743},
MONTH = {October},
PAGES = {14--28},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/csp-padl-final.pdf},
STUPSOLD = {44},
STUPSREV = {Plagge},
TITLE = {Design and Implementation of the High-Level Specification Language {CSP(LP)}},
VOLUME = {1990},
YEAR = {2001},
}
@INPROCEEDINGS{LeAdBuFeMi01_45,
ABSTRACT = {We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and tabling is a good foundation for developing, animating, and model checking new specification languages. We present animators and model checkers currently being developed for two different extensions of CSP and for the B method.},
AUTHOR = {Michael Leuschel and Laksono Adhianto and Michael Butler and Carla Ferreira and Leonid Mikhailov},
BOOKTITLE = {Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic},
EDITOR = {Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche},
MONTH = {September},
PAGES = {97--109},
STUPSOLD = {45},
STUPSREV = {Plagge},
TITLE = {Animation and Model Checking of {CSP} and {B} using {Prolog} Technology},
YEAR = {2001},
}
@INPROCEEDINGS{LeMaCu01_46,
ABSTRACT = {We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying certain temporal properties. To remedy this problem, we show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between ``classical'' model checking and refinement checking.},
AUTHOR = {Michael Leuschel and Thierry Massart and Andrew Currie},
BOOKTITLE = {Proceedings FME'2001},
EDITOR = {J.N. Oliviera, P. Zave},
MONTH = {March},
PAGES = {99--118},
PUBLISHER = {Springer-Verlag},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/fme2001-final.pdf},
STUPSOLD = {46},
STUPSREV = {leuschel},
TITLE = {How to make FDR Spin: LTL model checking of CSP using Refinement},
YEAR = {2001},
}
@PROCEEDINGS{LePoRaUl01_47,
EDITOR = {Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche},
MONTH = {September},
STUPSOLD = {47},
STUPSREV = {Plagge},
TITLE = {Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001},
YEAR = {2001},
}
@INPROCEEDINGS{LeWoMaAd01_48,
ABSTRACT = {We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present a technique to perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We present a tool which automates the translation process from LTL model checking to CSP refinement. Also, if time permits, we will present another tool which uses latest generation Prolog technology to symbolically animate, compile, and model check CSP specifications.},
AUTHOR = {Michael Leuschel and Ivan Wolton and Thierry Massart and Laksono Adhianto},
BOOKTITLE = {AVoCS 2001},
EDITOR = {David Nowak},
MONTH = {April},
PUBLISHER = {Oxford University Computing Laboratory},
STUPSOLD = {48},
STUPSREV = {Plagge},
TITLE = {Temporal Logic Model Checking of {CSP}: Tools and Techniques},
YEAR = {2001},
}
@THESIS{Ha01_301,
ABSTRACT = {We introduce the probabilistic action system formalism which combines refinement with performance. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. Corresponding notions of refinement and simulation-based proof rules are introduced. Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification AA to a more deterministic concrete specification CC. Knowing AA and CC one proves CC refines, or implements, specification AA. In this study we consider specification AA as given and concern ourselves with a way to find a good candidate for implementation CC. To this end we classify all implementations of an abstract specification according to their performance. The performance of a specification AA is a value val.AA associated with some optimal behaviour it may exhibit. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification are excluded. Only the remaining correct implementations CC are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary val.AA for the performance of any implementation. An implementation may perform worse than its specification but never better. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification AA, and the associated value val.AA, thus assisting in the search for a good implementation CC. We present examples and case studies to demonstrate the use of probabilistic action systems.},
AUTHOR = {Stefan Hallerstede},
DBSLINKS = {[http://eprints.ecs.soton.ac.uk/9294/|PDF]},
INSTITUTION = {Electronics and Computer Science, University of Southampton},
STUPSOLD = {301},
STUPSREV = {Hallerstede},
TITLE = {Performance-Oriented Refinement},
TYPE = {phdthesis},
YEAR = {2001},
}
@REPORT{LeLe02_36,
ABSTRACT = {Ecce is a partial deduction system which can be used to automatically generate abstractions for the model checking of many infinite state systems. We show that to verify the abstractions generated by Ecce we may employ the proof assistant Isabelle. Thereby Ecce is used to generate the specification, hypotheses and proof script in Isabelle's theory format. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of Ecce's abstraction. In this work we focus on the specification and verification of Petri nets.},
AUTHOR = {Helko Lehmann and Michael Leuschel},
INSTITUTION = {ECS, University of Southampton},
MONTH = {September},
NUMBER = {DSSE-TR-2002-02},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/is-tr.dsse-2002-2.pdf},
STUPSOLD = {36},
STUPSREV = {Plagge},
TITLE = {Generating inductive verification proofs for {Isabelle} using the partial evaluator {Ecce}},
TYPE = {techreport},
YEAR = {2002},
}
@INPROCEEDINGS{Le02_37,
ABSTRACT = {Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of techniques for program analysis, specialisation, transformation, and verification. In this paper we survey and discuss this use of homeomorphic embedding and clarify the advantages of such an approach over one using well-founded orders. We also discuss various extensions of the homeomorphic embedding relation. We conclude with a study of homeomorphic embedding in the context of metaprogramming, presenting some new (positive and negative) results and open problems.},
AUTHOR = {Michael Leuschel},
BOOKTITLE = {The Essence of Computation -- Essays dedicated to Neil Jones},
EDITOR = {Torben Mogensen, David Schmidt, I. H. Sudborough},
ISBN = {3-540-00326-6},
PAGES = {379--403},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/state-of-the-art.final.pdf},
STUPSOLD = {37},
STUPSREV = {Plagge},
TITLE = {Homeomorphic Embedding for Online Termination of Symbolic Methods},
VOLUME = {2566},
YEAR = {2002},
}
@ARTICLE{LeBr02_38,
ABSTRACT = {Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known respectively as partial evaluation and partial deduction, is to exploit partial knowledge about the input. It is achieved through a well-automated application of parts of the Burstall-Darlington unfold/fold transformation framework. The main challenge in developing systems is to design automatic control that ensures correctness, efficiency, and termination. This survey and tutorial presents the main developments in controlling partial deduction over the past 10 years and analyses their respective merits and shortcomings. It ends with an assessment of current achievements and sketches some remaining research challenges.},
AUTHOR = {Michael Leuschel and Maurice Bruynooghe},
ISSN = {1471-0684},
JOURNALTITLE = {Theory and Practice of Logic Programming},
MONTH = {July},
NUMBER = {4--5},
PAGES = {461--515},
PUBLISHER = {Cambridge University Press},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/pdcontrol.tplpfinal.pdf},
STUPSOLD = {38},
STUPSREV = {Plagge},
TITLE = {Logic program specialisation through partial deduction: Control Issues},
VOLUME = {2},
YEAR = {2002},
}
@INPROCEEDINGS{LeGr02_39,
ABSTRACT = {We present an abstract partial deduction technique which uses regular types as its domain and which can handle conjunctions, and thus perform deforestation and tupling. We provide a detailed description of all the required operations and present an implementation within the Ecce system. We discuss the power of this new specialisation algorithm, especially in the light of verifying and specialising infinite state process algebras. Here, our new algorithm can provide a more precise treatment of synchronisation and can be used for refinement checking. Paper Available: http://link.springer.de/link/service/series/0558/tocs/t2372.htm#toc2372},
AUTHOR = {Michael Leuschel and Stefan Gruner},
BOOKTITLE = {LOPSTR},
EDITOR = {Alberto Pettorossi},
ISBN = {3-540-43915-3},
PAGES = {91--110},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {39},
STUPSREV = {Plagge},
TITLE = {Abstract Conjunctive Partial Deduction using Regular Types and its Application to Model Checking},
VOLUME = {2372},
YEAR = {2002},
}
@INPROCEEDINGS{LeMa02_40,
ABSTRACT = {In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming.<br/> This approach is flexible in the sense that various specification formalisms can be easily targeted (e.g., Petri nets, CSP, ...). Moreover, infinite state CTL model checking can be performed by analysing this interpreter using a combination of partial deduction and abstract interpretation. It has also been shown that this approach is powerful enough to decide coverability properties of various kinds of Petri nets. <br/> In this ongoing work, we are empirically evaluating these approaches on various case studies of finite, parameterised and infinite systems. For finite state systems, we show how our approach and tool compares to standard tools for finite state model checking For parameterised or infinite state model checking, we are comparing our results with, e.g., XMC, Hytech.},
AUTHOR = {Michael Leuschel and Thierry Massart},
BOOKTITLE = {AVoCS},
EDITOR = {Gethin Norman and Martha Kwiatkowska and Dimitar Guelev},
PAGES = {143--149},
PUBLISHER = {University of Birmingham},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/Avocs2002.pdf},
STUPSOLD = {40},
STUPSREV = {Plagge},
TITLE = {Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation},
YEAR = {2002},
}
@INPROCEEDINGS{VaAlLe02_41,
AUTHOR = {Mauricio Varea and Bashir Al-Hashimi and Michael Leuschel},
BOOKTITLE = {AVoCS},
MONTH = {April},
PAGES = {265--269},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/Birmingham.pdf},
STUPSOLD = {41},
STUPSREV = {Plagge},
TITLE = {Finite and Infinite Model Checking of Dual Transition Petri Net Models},
YEAR = {2002},
}
@PROCEEDINGS{02_100,
EDITOR = {Michael Leuschel},
ISBN = {3-540-40438-4},
ISSN = {0302-9743},
SERIES = {Lecture Notes in Computer Science},
STUPSOLD = {100},
STUPSREV = {Plagge},
TITLE = {Logic Based Program Synthesis and Transformation, Proceedings of LOPSTR'02, Revised Selected Papers},
VOLUME = {2664},
YEAR = {2002},
}
@PROCEEDINGS{02_101,
EDITOR = {Michael Leuschel and Ultes-Nitsche, Ulrich},
STUPSOLD = {101},
STUPSREV = {Plagge},
TITLE = {Proceedings of the ACM Sigplan International Workshop on Verification and Computational Logic (VCL'2002)},
YEAR = {2002},
}
@INPROCEEDINGS{Ha02_293,
ABSTRACT = {Stepwise refinement transforms an abstract specification into a more deterministic concrete specification. Ultimately one arrives at a specification that is implementable. At the various stages in the refinement process decisions are made that determine how the final implementation operates. Different implementations can be compared with respect to their expected performance within their environment. In this sense refinement poses an optimisation problem. We present a B-based language and a tool that can assist in solving this optimisation problem.},
AUTHOR = {Stefan Hallerstede and Michael Butler},
BOOKTITLE = {RCS '02: International Workshop on Refinement of Critical Systems: Methods, Tools and Experience},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/rcs02-performanceoriented.pdf},
STUPSOLD = {293},
STUPSREV = {Hallerstede},
TITLE = {A Performance-oriented Refinement Assistant},
YEAR = {2002},
}
@INPROCEEDINGS{AuFeGrLeNG03_24,
AUTHOR = {Juan Carlos Augusto and Carla Ferreira and Andy M. Gravell and Michael Leuschel and Karen M.Y. Ng},
BOOKTITLE = {ER (Workshops)},
EDITOR = {Manfred A. Jeusfeld and Oscar Pastor},
ISBN = {3-540-20257-9},
PAGES = {17--28},
PUBLISHER = {Springer Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/ecomo.pdf},
STUPSOLD = {24},
STUPSREV = {Plagge},
TITLE = {The Benefits of Rapid Modelling for E-Business System Development},
VOLUME = {2814},
YEAR = {2003},
}
@INPROCEEDINGS{AuLeBuFe03_25,
AUTHOR = {Juan Carlos Augusto and Michael Leuschel and Michael Butler and Carla Ferreira},
BOOKTITLE = {AVoCS},
EDITOR = {Michael Leuschel and Stefan Gruner and Stephane Lo Presti},
PAGES = {253--266},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/avocs03.pdf},
STUPSOLD = {25},
STUPSREV = {Plagge},
TITLE = {Using the Extensible Model Checker {XTL} to Verify {StAC} Business Specifications},
YEAR = {2003},
}
@ARTICLE{BuLeLoAlBeBoCuKi03_26,
ABSTRACT = {We present a scheme for highlighting the trust issues of merit within pervasive computing, based on an analysis of scenarios from the healthcare domain. The first scenario helps us define an analysis grid, where the human and technical aspects of trust are considered. The analysis is applied to a second scenario to examine its suitability. We then discuss the various categories of the analysis grid in the light of this examination and of the literature on the subject of trust. We believe that this approach could form the basis of a generalised trust analysis framework to support the design, procurement and use of pervasive computing. (The PDF is an extended version of the paper.)},
AUTHOR = {Michael Butler and Michael Leuschel and Stephane Lo Presti and David Allsopp and Patrick Beautement and Chris Booth and Mark Cusack and Mike Kirton},
JOURNALTITLE = {IEEE Computing},
NUMBER = {3},
PAGE = {96},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/aamas-workshop03.pdf},
STUPSOLD = {26},
STUPSREV = {leuschel},
TITLE = {Towards a Trust Analysis Framework for Pervasive Computing Scenarios},
VOLUME = {2},
YEAR = {2003},
}
@INPROCEEDINGS{CrLe03_27,
ABSTRACT = {The Cogen approach to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success. This paper demonstrates that the Cogen approach is also applicable to the specialisation of constraint logic programs and leads to effective specialisers. We present the basic specialisation technique for CLP(Q) programs and show how we can handle non-declarative features as well. We present an implemented system along with experimental results.},
AUTHOR = {Stephen Craig and Michael Leuschel},
BOOKTITLE = {Ershov Memorial Conference},
EDITOR = {M. Broy and A. Zamulin},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
STUPSFILE = {http://www.stups.uni-duesseldorf.de/publications/clp-final.ps},
STUPSOLD = {27},
STUPSREV = {Plagge},
TITLE = {A Compiler Generator for Constraint Logic Programs},
VOLUME = {2890},
YEAR = {2003},
}
@INPROCEEDINGS{DBLP:conf/gpce/ElphickLC03,
ABSTRACT = {We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like MATLAB and then propose partial evaluation as a way of lessening the disadvantages at little cost. We then go on to describe the design of a partial evaluator for MATLAB and present results showing what performance increases can be achieved and the circumstances in which partial evaluation can provide these.},
AUTHOR = {Daniel Elphick and Michael Leuschel and Simon J. Cox},
BIBSOURCE = {dblp computer science bibliography, http://dblp.org},
BIBURL = {http://dblp.uni-trier.de/rec/bib/conf/gpce/ElphickLC03},
BOOKTITLE = {Generative Programming and Component Engineering, Second International Conference, {GPCE} 2003, Erfurt, Germany, September 22-25, 2003, Proceedings},
CROSSREF = {DBLP:conf/gpce/2003},
DOI = {10.1007/978-3-540-39815-8_21},
PAGES = {344--363},
TIMESTAMP = {Tue, 05 Jul 2011 17:29:49 +0200},
TITLE = {Partial Evaluation of {MATLAB}},
URL = {http://dx.doi.org/10.1007/978-3-540-39815-8_21},
YEAR = {2003},
}
@PROCEEDINGS{DBLP:conf/gpce/2003,
BIBSOURCE = {dblp computer science bibliography, http://dblp.org},
BIBURL = {http://dblp.uni-trier.de/rec/bib/conf/gpce/2003},
EDITOR = {Frank Pfenning and Yannis Smaragdakis},
ISBN = {3-540-20102-5},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
TIMESTAMP = {Wed, 19 Nov 2003 15:46:51 +0100},
TITLE = {Generative Programming and Component Engineering, Second International Conference, {GPCE} 2003, Erfurt, Germany, September 22-25, 2003, Proceedings},
VOLUME = {2830},