No abstract available.
Cited By
- Méry D and Singh N Automatic code generation from event-B models Proceedings of the 2nd Symposium on Information and Communication Technology, (179-188)
- Barnett M, Leino K and Schulte W The spec# programming system Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, (49-69)
- Maurer W The modification index method of generating verification conditions Proceedings of the 15th annual Southeast regional conference, (426-440)
- Rosen B (1977). High-level data flow analysis, Communications of the ACM, 20:10, (712-724), Online publication date: 1-Oct-1977.
- Cousot P and Cousot R Abstract interpretation Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, (238-252)
- Katz S and Manna Z (1976). Logical analysis of programs, Communications of the ACM, 19:4, (188-206), Online publication date: 1-Apr-1976.
- Wegbreit B (1975). Mechanical program analysis, Communications of the ACM, 18:9, (528-539), Online publication date: 1-Sep-1975.
- King J (1975). A new approach to program testing, ACM SIGPLAN Notices, 10:6, (228-233), Online publication date: 1-Jun-1975.
- London R (2019). A view of program verification, ACM SIGPLAN Notices, 10:6, (534-545), Online publication date: 1-Jun-1975.
- King J A new approach to program testing Proceedings of the international conference on Reliable software, (228-233)
- London R A view of program verification Proceedings of the international conference on Reliable software, (534-545)
Recommendations
Proving termination properties with MU-TERM
AMAST'10: Proceedings of the 13th international conference on Algebraic methodology and software technologyMU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted rewriting, termination of context-...
Proving operational termination of membership equational programs
Reasoning about the termination of equational programs in sophisticated equational languages such as Elan , Maude , OBJ , CafeOBJ , Haskell , and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of ...
Proving termination of (conditional) rewrite systems
In this paper an important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a ...