Alberto Pettorossi and Maurizio Proietti and Valerio Senni (2009):
Deciding Full Branching Time Logic by Program Transformation.
In: 19th International Symposium on Logic-Based Program Synthesis and Transformation,
pp. 5–21,
doi:10.1007/978-3-642-12592-8_2.
Alexei Lisitsa and Andrei P. Nemytykh (2008):
Reachability Analysis in Verification via Supercompilation.
International Journal of Foundations of Computer Science 19(4),
pp. 953–969,
doi:10.1142/S0129054108006066.
E.M. Clarke, E.A. Emerson & A.P. Sistla (1986):
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.
ACM Transactions on Programming Languages and Systems 8(2),
pp. 244–263,
doi:10.1145/5397.5399.
Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti (2001):
Verification of Sets of Infinite State Processes Using Program Transformation.
In: 11th International Workshop on Logic Based Program Synthesis and Transformation,
pp. 111–128,
doi:10.1007/3-540-45607-4_7.
G.W. Hamilton (2007):
Distillation: Extracting the Essence of Programs.
In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation,
pp. 61–70,
doi:10.1145/1244381.1244391.
G.W. Hamilton (2015):
Verifying Temporal Properties of Reactive Systems by Transformation.
Electronic Proceedings of Theoretical Computer Science 199,
pp. 33–50,
doi:10.4204/EPTCS.199.
G.W. Hamilton & N.D. Jones (2012):
Distillation With Labelled Transition Systems.
In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation.
ACM,
pp. 15–24,
doi:10.1145/2103746.2103753.
Hirohisa Seki (2011):
Proving Properties of Co-Logic Programs by Unfold/Fold Transformations.
In: 21st International Symposium on Logic-Based Program Synthesis and Transformation,
pp. 205–220,
doi:10.1007/978-3-642-32211-2_14.
L. Lamport (1974):
A New Solution of Dijkstra's Concurrent Programming Problem.
Communications of the ACM 17(8),
pp. 453–455,
doi:10.1145/361082.361093.
Lester, M.M. and Neatherway, R.P. and Ong, C.-H. L. and Ramsay, S.J. (2010):
Model Checking Liveness Properties of Higher-Order Functional Programs.
Unpublished.
M. Leuschel & T. Massart (1999):
Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
In: 9th International Workshop on Logic Programming Synthesis and Transformation,
pp. 62–81,
doi:10.1007/10720327_5.
A. Lisitsa & A. Nemytykh (2007):
Verification as a Parameterized Testing (Experiments with the SCP4 Supercompiler).
Programming and Computer Software 33(1),
pp. 14–23,
doi:10.1134/S0361768807010033.
Naoki Kobayashi (2009):
Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs.
In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL,
pp. 416–428,
doi:10.1145/1480881.1480933.
C.-H. L. Ong (2006):
On Model-Checking Trees Generated by Higher-Order Recursion Schemes.
In: Proceedings of Logic in Computer Science, LICS.
IEEE Computer Society Press,
pp. 81–90,
doi:10.1109/LICS.2006.38.
Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan & Scott A. Smolka (2000):
Verification of Parameterized Systems Using Logic Program Transformations.
In: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems,
pp. 172–187,
doi:10.1007/3-540-46419-0_13.
M.H. Sørensen, R. Glück & N.D. Jones (1996):
A Positive Supercompiler.
Journal of Functional Programming 6(6),
pp. 811–838,
doi:10.1017/S0956796800002008.
V.F. Turchin (1986):
The Concept of a Supercompiler.
ACM Transactions on Programming Languages and Systems 8(3),
pp. 90–121,
doi:10.1145/5956.5957.
eptcs@eptcs.org