Mathematics of Program Construction ; 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings
This book constitutes the refereed proceedings of the 9th International Conference on Mathematics of Program Construction, MPC 2008, held in Marseille, France in July 2008.The 18 revised full papers presented together with 1 invited talk were carefully reviewed and selected from 41 submissions. Issues addressed range from algorithmics to support for program construction in programming languages and systems. Topics of special interest are type systems, program analysis and transformation, programming language semantics, program logics.
Constructing Correct Software
Central to Formal Methods is the so-called Correctness Theorem which relates a specification to its correct Implementations. This theorem is the goal of traditional program testing and, more recently, of program verification (in which the theorem must be proved). Proofs are difficult, though even with the use of powerful theorem provers. This volume explains and illustrates an alternative method, which allows the construction of (necessarily correct) algorithms from a specification using algebraic transformations and refinement techniques which prevent the introduction of errors. Based on teaching material used extensively at Loughborough University, John Cooke introduces the basics, using simple examples and lots of detailed working (which can often be re-used). Constructing Correct Software will provide invaluable reading for students and practitioners of Computer Science and Software Engineering to whom correctness of software is of prime importance.
CONCUR 2008 - Concurrency Theory ; 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings
This book constitutes the refereed proceedings of the 19th International Conference on Concurrency Theory, CONCUR 2008, held in Toronto, Canada, August 19-22, 2008.
Logic for Computer Scientists
This book introduces the notions and methods of formal logic from a computer science standpoint, covering propositional logic, predicate logic, and foundations of logic programming. It presents applications and themes of computer science research such as resolution, automated deduction, and logic programming in a rigorous but readable way.The style and scope of the work, rounded out by the inclusion of exercises, make this an excellent textbook for an advanced undergraduate course in logic for computer scientists.
Logic Based Program Synthesis and Transformation ; Vol. 3901 ; 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers
This book constitutes the thoroughly refereed post-proceedings of the 15th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2005, held in September 2005. The papers are organized in topical sections on tools for program development, program transformations, and software development and program analysis.
Logic Based Program Synthesis and Transformation ; Vol. 3573 : 14th International Symposium, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers
In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logic program. The presence of duplicated code (or functionality) is a primary indication that the design of the program can be improved by performing a so-called refactoring transformation. Within the framework of our analysis, we formally characterize three situations of duplicated functionality and their associated refactorings: the extraction of a duplicated goal into a new predicate, the removal of equivalent predicates and the generalization of two predicates into a higher-order predicate. The resulting analysis detects in a completely automatic way what program fragments are suitable candidates for the considered refactoring transformations.
Automated deduction – CADE 28 ; 28th International Conference on automated deduction, Virtual Event, July 12–15, 2021, Proceedings
This book constitutes the proceeding of the 28th International Conference on Automated Deduction, CADE 28, held virtually in July 2021. The 29 full papers and 7 system descriptions presented together with 2 invited papers were carefully reviewed and selected from 76 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. The papers are organized in the following topics: Logical foundations; theory and principles; implementation and application; ATP and AI; and system descriptions.






