Page 3
Page 3
Verified Software: Theories, Tools, Experiments ; 1st IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions
The book includes a general introduction to the area, which also presents the vision of a grand challenge project: the "verifying compiler". Most contributions are followed by a transcription of the vivid discussion that ensued between the author and the audience. The papers have been organized in topical sections on verification tools, guaranteeing correctness, software engineering aspects, verifying object-oriented programming, programming language and methodology aspects, components, static analysis, design, analysis and tools, as well as formal techniques.
Verification, Model Checking, and Abstract Interpretation ; Vol. 3855 ; 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings
Contains the papers accepted for presentation at the 7th Interna-tional Conference on Verification, Model Checking, and Abstract Interpretation,held January 8-10, 2006, at Charleston, South Carolina, USA.VMCAI provides a forum for researchers from the communities of verifica-tion, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods.The program was selected from 58 submitted papers.
Verification, model checking, and abstract interpretation ; Vol. 3385 ; 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings
The 27 revised full papers presented here, together with one invited paper were carefully reviewed and selected from 58 submissions. The papers feature current research from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods.
Verification, Model Checking, and Abstract Interpretation ; 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008. Proceedings
The book feature current research from the communities of verification, program certification, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, cross-fertilization, and advancement of hybrid methods.
Verification, Model Checking, and Abstract Interpretation ; 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings
Contains the papers presented at VMCAI 2007: Verification, Model Checking and Abstract Interpretation held January 14–16, 2007 in Nice. VMCAI provides a forum for researchers from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization,and dvancement of hybrid methods that combine the three areas.
Verification, Model Checking, and Abstract Interpretation ; 3rd International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers
This volume contains the revised version of papers presented at VMCAI 2002,the Third International Workshop on Verification, Model Checking, and AbstractInterpretation, Venice (Italy), January 21-22, 2002.The main goal of the workshop was to give an overview of the main directionsdecisive for the growth and cross-fertilization of major research activities inprogram analysis and verification. The program committee selected 22 papers out of 41 submissions on the basisof at least 3 reviews. The resulting volume offers the reader an interesting perspectiveof the current research trends in the area. In particular, the papers contributeto the following topics: Security and Protocols, Timed Systems and Games,Static Analysis, Optimizations, Types and Verification, and Temporal Logicsand Systems.
Verification of Object-Oriented Software : The KeY Approach
Features of the programming languages we employ in these programs are plentiful, including object-oriented organizations of data, facilities for specifying di?erent c- trol ?ow for rare situations, constructs for iterating over the elements of a collection, and the grouping together of operations into atomic transactions. These language features were designed to facilitate simpler and more natural encodings of programs, and ideally they are accompanied by simpler proof rules. But the variety and increased number of these features make it harder to remember all that needs to be proved about their uses. As a third problem, we have come to expect a higher degree of rigor from our proofs. A proof carried out or replayed by a machine somehow gets more credibility than one that requires human intellect to understand.
Venezuela : A Petro-State Using Renewable Energies : A Contribution to the Global Debate about New Renewable Energies for Electricity Generation
In spite of the economic role of oil, Venezuela has started developing hydroelectricity since the 1950s. At present, the country is trying to introduce additional renewable energy sources (RES) but still has to overcome a series of hurdles in order to deploy them. Unlike other developing countries, oil countries such as Venezuela do not lack financial means and sometimes show a tendency to solve problems by using money when other approaches could be more helpful. The main goal of this qualitative, comparative policy analysis is to find out whether the availability of oil revenues restraints or favors the adoption of RES. Based on the rentier state theory, Germán Massabié examines the reasons why Petro states try to dispose of their natural wealth to take advantage of non-conventional energy sources. He analyses and interprets primary and secondary data collected in Germany and in Venezuela and draws on interviews with Venezuelan experts, policy makers, and key actors. The study allows a look beyond laws, development programs, and official statements.
Vehicle Propulsion Systems : Introduction to Modeling and Optimization ; 2nd ed.
Automobiles are responsible for a substantial part of the world's consumption of primary energy, mostly fossil liquid hydrocarbons. The reduction of the fuel consumption of these vehicles has become a top priority. Many ideas to reach that objective have been presented. In most cases these systems are more complex than the traditional approaches. For such complex systems a heuristic design approach fails. The only way to deal with this situation is to employ model-based methods. This text provides an introduction to the mathematical modeling and subsequent optimization of vehicle propulsion systems and their supervisory control algorithms.
VEE Pro : Practical Graphical Programming
Each of the 18 lessons introduces new programming objects, concepts or techniques that can be presented in a whole-group session or studied privately prior to the labs in the classes proper. These prelabs are collected in a separate appendix so that your assimilation of novel material does not interrupt the practical lesson flow and can be easily referenced when you are devising a new program.You will see the power and flexibility of VEE Pro in action in special labs of increasing complexity based around the monitoring and control of a virtual vehicle radiator.
Variations on Constants : Flow Analysis of Sequential and Parallel Programs
This monograph, a revised version of the author's habilitation thesis, focusses on optimal flow analysis of sequential and parallel programs. It studies algorithmic properties of various versions of the well-known constant-propagation problem. In order to come to grips with the variants considered, it combines techniques from different areas such as linear algebra, computable ring theory, abstract interpretation, program verification, complexity theory, etc. Combination of techniques is the key to further progress in automatic analysis and constant-propagation allows us to illustrate this point in a theoretical study.
Valuing Agroforestry Systems : Methods and Applications
Offers practical means for strengthening the economics and policy dimension of the agroforestry discipline. The applied economic methodologies encompass a wide variety of case studies including enterprise/farm budget models through Faustmann models, Policy Analysis Matrix, production function approach, risk assessment models, dynamic programming, linear programming, meta-modeling, contingent valuation, attribute-based choice experiments, econometric modeling, and institutional economic analysis. It is our belief that these methodologies help agroforestry students and professionals conduct rigorous assessment of economic and policy aspects of agroforestry systems and to produce less biased and more credible information. Furthermore, the economic and policy issues explored in the book – profitability, environmental benefits, risk reduction, household constraints, rural development, and institutional arrangements – are central to further agroforestry adoption in both tropical and temperate regions
Values Education and Lifelong Learning : Principles, Policies, Programmes
The aim of this book is to provide an easily accessible, practical yet scholarly source of information about the international concern for the nature, theory and practices of the ideas of values education and lifelong learning.
Value-Range Analysis of C Programs : Towards Proving the Absence of Buffer Overflow Vulnerabilities
The use of static analysis techniques to prove the partial correctness of C code has recently attracted much attention due to the high cost of software errors - particularly with respect to security vulnerabilities. However, research into new analysis techniques is often hampered by the technical difficulties of analysing accesses through pointers, pointer arithmetic, coercion between types, integer wrap-around and other low-level behaviour. Axel Simon provides a concise, yet formal description of a value-range analysis that soundly approximates the semantics of C programs using systems of linear inequalities (polyhedra). The analysis is formally specified down to the bit-level while providing a precise approximation of all low-level aspects of C using polyhedral operations and, as such, it provides a basis for implementing new analyses that are aimed at verifying higher-level program properties precisely. One example of such an analysis is the tracking of the NUL position in C string buffers, which is shown as an extension to the basic analysis and which thereby demonstrates the modularity of the approach.
Validated Designs for Object-oriented Systems
Describes an object-oriented design approach that combines the benefits of abstract modelling with the analytic power of formal methods, to give designs that can be rigorously validated & assured with automated support. Aimed at software architects, designers & developers as well as computer scientists, no prior knowledge of formal methods is assumed. The elements of functional modelling are introduced using numerous examples & exercises, industrial case studies & experience reports. Industry-strength tools support the text.
Using Algebraic Geometry
In recent years, the discovery of new algorithms for dealing with polynomial equations, coupled with their implementation on fast inexpensive computers, has sparked a minor revolution in the study and practice of algebraic geometry. These algorithmic methods have also given rise to some exciting new applications of algebraic geometry. This book illustrates the many uses of algebraic geometry, highlighting some of the more recent applications of Gröbner bases and resultants.
Uses of technology in upper secondary mathematics education
This survey addresses the use of technology in upper secondary mathematics education from four points of view: theoretical analysis of epistemological and cognitive aspects of activity in new technology mediated learning environments, the changes brought by technology in the interactions between environment, students and teachers, the interrelations between mathematical activities and technology, skills and competencies that must be developed in teacher education. Research shows that the use of some technologies may deeply change the solving processes and contribute to impact the learning processes. The questions are which technologies to choose for which purposes, and how to integrate them, so as to maximize all students’ agency. In particular the role of the teacher in classrooms and the content of teacher education programs are critical for taking full advantage of technology in teaching practice.
Use Case Driven Object Modeling with UML : Theory and Practice
Use Case Driven Object Modeling with UML: Theory and Practice shows how to drive an object-oriented software design from use case all the way through coding and testing, based on the minimalist, UML-based ICONIX process. In addition to a comprehensive explanation of the foundations of the approach, the book makes extensive use of examples and provides exercises at the back of each chapter.
US Spacesuits
Successfully meeting the challenges to creating safe, reliable and comfortable spacesuits is an ongoing effort that has spanned over four decades. The book includes over 100 design models and 13 manufacturers that have thus far supported civilian and defense spacesuit programs." "Both authors have unparalleled experience in US spacesuit development, and this ensures a technically accurate and historically interesting text. The book is also illustrated by a unique collection that includes scores of never previously reproduced photographs. US Spacesuits is the most accurate and comprehensive text about the general topic of spacesuits, and US spacesuits in particular, that has ever been produced.
Urban Transportation Planning in the United States : History, Policy, and Practice
The book focuses in-depth at the most significant event in transportation planning--the Federal-Aid Highway Act of 1962; creating a federal mandate for a comprehensive urban transportation planning process carried out cooperatively by states and local governments with federal funding, this act was crucial in the spread of urban transportation. Claiming that urban transportation planning is more sophisticated, costly, and complex than its highway and transit planning predecessors, the book demonstrates how urban transportation planning evolved in response to changes in such factors as environment, energy, development patterns, intergovernmental coordination, and federal transit programs. It further illustrates how broader concerns for global climate change and sustainable development have braided the purview of transportation planning. This fully updated, revised, and expanded edition highlights the dynamics of transportation planning post-9/11, covers the impact of recent legislation, emphasizes such timely issues as security, oil dependence, performance measurement, and public-private sector collaboration.
