Formal Methods and Software Engineering: 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings
Jin Song Dong, Huibiao Zhu
Springer Science & Business Media, Oct 29, 2010 - Computers - 712 pages
Formal methods have made signi?cant progress in recent years with succe- ful stories from Microsoft (SLAM project), Intel (i7 processor veri?cation) and NICTA/OK-Lab (formal veri?cation of an OS kernel). The main focus of f- malengineeringmethodsliesinhowformalmethodscanbee?ectivelyintegrated intomainstreamsoftwareengineering.Variousadvancedtheories,techniquesand tools havebeen proposed, developed and applied in the speci?cation, design and veri?cation of software or in the construction of software. The challenge now is how to integrate them into engineering development processes to e?ectively deal with large-scale and complex computer systems for their correct and - ?cient construction and maintenance. This requires us to improve the state of the art by researching e?ective approaches and techniques for integration of f- mal methods into industrial engineering practice, including new and emerging practice. Thisseries,InternationalConferencesonFormalEngineeringMethods,brings together those interested in the application of formal engineering methods to computer systems. This volume contains the papers presented at ICFEM 2010, the 12th International Conference on Formal Engineering Methods, held November 17–19, in Shanghai, China, in conjunction with the Third Inter- tional Symposium on Unifying Theories of Programming (UTP 2010). The Program Committee received 114 submissions from 29 countries and - gions. Each paper was reviewed by at least three program committee members.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
abstract algorithm analysis applied approach automated automatically behavior CafeOBJ checker clock component composition Computer concurrent condition conﬁguration constraints construction context deadlock deﬁned deﬁnition denoted diagram diﬀerent domain equations example execution expression fault fault injection ﬁnd ﬁnite ﬁrst ﬂow formal formal verification formula fUML function heapsort Heidelberg identiﬁed IEEE implementation inﬁnite initial input instance interface label language lemma LNCS lock metaclass metamodel method metric model checking module node NUSMV operational semantics operator parameterised parameters pattern Petri net postcondition predicate problem frame procedure processor proof scores properties protocol prove queue reachable recursive reﬁnement relation represented result satisﬁes Section semantics sequence slicing soft error speciﬁcation Specs Springer structure symbolic synchronous technique temporal logic theorem tion tool transition transition relation tuple variables veriﬁcation verify WS-CDL WSMO