Property-oriented expansion

1. A.V. Aho, R. Sethi, J.D. Ullman. Compilers: Principles, Techniques and Tools, Addison-Wesley, 1985.

   Google Scholar 

2. J. Bradfield, C.Stirling. Local Model Checking for Infinite State Spaces. LFCS Report Series ECS-LFCS-90-115, June 1990

   Google Scholar 

3. P. Cousot, R. Cousot. Abstract interpretation: A unified Lattice Model for static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings 4th POPL, Los Angeles, California, January, 1977

   Google Scholar 

4. C. Click, K.D. Cooper. Combining Anlyses, Combining Optimizations, ACM TOPLAS N.2, Vol.17, pp.181–196, 1995

   Google Scholar 

5. E. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In Proceedings 10th POPL'83, 1983

   Google Scholar 

6. C. Click. Combining Analyses, Combining Optimizations, Ph.D. Thesis, Rice University, Houston, TX, 1995, 149 pages.

   Google Scholar 

7. E. Emerson, J. Lei, Efficient model checking in fragments of the propositional mu-calculus. In Proceedings LICS'86, 267–278, 1986

   Google Scholar 

8. R. Giegerich, U. Möncke, R. Wilhelm. Invariance of Approximative Semantics with Respect to Program Transformations, Informatik-Fachberichte 50, pp. 1–10, Proc. of the third Conference of the European Co-operation in Informatics, Springer, 1981.

   Google Scholar 

9. P. Godefroit. Partial-Order Methods for the Verification of Concurrent Systems. LNCS Monography, LNCS 1032, 1996.

   Google Scholar 

10. S. Horwitz, A. Demers, T. Teitelbaum. An Efficient General Iterative Algorithm for Data Flow Analysis, Acta Informatica, vol. 24, pp. 679–694, 1987.

    MathSciNet  Google Scholar 

11. G. A. Kildall. A unified approach to global program optimization. In Conf. Rec. 1st ACM Symposium on Principles of Programming Languages (POPL'73), pages 194–206. ACM, New York, 1973.

    Google Scholar 

12. M. Klein, J. Knoop, D. Koschützki, B. Steffen. DFA & OPT-MetaFrame: A Toolkit for Program Analysis and Optimization (Tool description) — Proc. TACAS'96, Int. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, LNCS 1055 Springer, pp. 418–421

    Google Scholar 

13. D. Kozen. Results on the Propositional mu-Calculus. TCS 27, 333–354, 1983

    Google Scholar 

14. J. Knoop, O. Rüthing, B. Steffen. Partial Dead Code Elimination, SIGPLAN PLDI Conference'94, ACM SIGPLAN Notices 29, Orlando, June 1994

    Google Scholar 

15. J. Knoop, O. Rüthing, B. Steffen. The Power of Assignment Motion, Proc. of the ACM SIGPLAN'95 Conference on Programming Language Design and Implemantion (PLDI'95), La Jolla, California, June 1995, SIGPLAN Notices 30, 6 (1995), 233–245

    Google Scholar 

16. Z. Manna, P. Wolper. “Synthesis of Communicating Processes from Temporal Logic Specifications,∝ ACM TOPLAS Vol.6, N.1, Jan. 1984, pp.68–93.

    Google Scholar 

17. E. Morel, C. Renvoise. Global Optimization by Suppression of Partial Redundancies. Communications of the ACM 22, 96–103, 1979

    Article  Google Scholar 

18. N.D. Jones, F. Nielson. Abstract Interpretation: A Semantics-Based Tool for Program Analysis. In Handbook of Logics in Computer Science, Vol. 4, pp. 527–637, Oxford University Press, 1995.

    Google Scholar 

19. B.K. Rosen, M.N. Wegman, F.K. Zadeck. “Global Value Numbers and Redundant Computations∝. 15^th POPL, San Diego, California, 12–27, 1988

    Google Scholar 

20. B. Steffen, A.Ingolfsdottir. Characteristic Formulae for Finite State Processes, International Journal on Information and Computation, Vol. 110, No. 1, 1994

    Google Scholar 

21. A.P. Sistla, E.M. Clarke. “The Complexity of the Propositional Linear Temporal Logics,∝ Journal of the ACM, Vol.32, N.3, July 1985, pp.733–749.

    Google Scholar 

22. B. Steffen. Characteristic Formulae. Proceedings of the International Colloquium on Automata, Languages and Programming, ICALP'89, LNCS 372, 1989

    Google Scholar 

23. B. Steffen. Data Flow Analysis as Model Checking. Proceedings of the International Concerence on Theoretical Aspects of Computer Software, TACS'91, LNCS 526, 1991

    Google Scholar 

24. B. Steffen. Generating Data Flow Analysis Algorithms from Modal Specifications, International Journal on Science of Computer Programming, N. 21, 1993, pp. 115–139.

    Google Scholar 

25. B. Steffen, T. Margaria, A. Claßen. Heterogeneous Analysis and Verification for Distributed Systems, In “SOFTWARE: Concepts and Tools∝, vol. 17, N.1, pp. 13–25, Springer Verlag, 1996.

    Google Scholar 

26. A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, v. 5, 1955.

    Google Scholar 

27. D. Whitfield, M.L. Soffa. An Approach to Ordering Optimizing Transformations, Proc. 2nd ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (PPOPP), Seattle, Washington, SIGPLAN Notes 25,3, pp.137–147, March 1990.

    Google Scholar 

Download references