| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910783031303321 |
|
|
Autore |
Parkman Francis <1823-1893.> |
|
|
Titolo |
The Oregon Trail [[electronic resource] ] : adventures on the prairie in the 1840's / / by Francis Parkman |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Santa Barbara, : Narrative Press, 2001 |
|
|
|
|
|
|
|
Descrizione fisica |
|
1 online resource (343 p.) |
|
|
|
|
|
|
Soggetti |
|
Frontier and pioneer life - West (U.S.) |
Indians of North America - West (U.S.) - History - 19th century |
West (U.S.) Description and travel |
Oregon National Historic Trail |
California National Historic Trail |
West (U.S.) History To 1848 |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910892166703321 |
|
|
Titolo |
Contas Nacionais / Instituto Nacional de Estatística |
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Instituto Nacional de Estatística |
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Periodico |
|
|
|
|
|
3. |
Record Nr. |
UNINA9910767504603321 |
|
|
Titolo |
B 2007: Formal Specification and Development in B : 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings / / edited by Jacques Julliand, Olga Kouchnarenko |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2006.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XIII, 297 p.) |
|
|
|
|
|
|
Collana |
|
Programming and Software Engineering, , 2945-9168 ; ; 4355 |
|
|
|
|
|
|
Altri autori (Persone) |
|
JulliandJacques |
KouchnarenkoOlga |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computer programming |
Software engineering |
Computer science |
Machine theory |
Programming Techniques |
Software Engineering |
Computer Science Logic and Foundations of Programming |
Formal Languages and Automata Theory |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Invited Talks -- E-Voting and the Need for Rigourous Software Engineering – The Past, Present and Future -- Using B Machines for |
|
|
|
|
|
|
|
|
|
|
|
Model-Based Testing of Smartcard Software -- The Design of Spacecraft On-Board Software -- Regular Papers -- Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions -- Chorus Angelorum -- Augmenting B with Control Annotations -- Justifications for the Event-B Modelling Notation -- Automatic Translation from Combined B and CSP Specification to Java Programs -- Symmetry Reduction for B by Permutation Flooding -- Instantiation of Parameterized Data Structures for Model-Based Testing -- Verification of LTL on B Event Systems -- Patterns for B: Bridging Formal and Informal Development -- Time Constraint Patterns for Event B Development -- Modelling and Proof Analysis of Interrupt Driven Scheduling -- Refinement of Statemachines Using Event B Semantics -- Formal Transformation of Platform Independent Models into Platform Specific Models -- Refinement of eb 3 Process Patterns into B Specifications -- Security Policy Enforcement Through Refinement Process -- Integration of Security Policy into System Modeling -- Industrial Papers -- Experiences in Using B and UML in Industrial Development -- B in Large-Scale Projects: The Canarsie Line CBTC Experience -- A Tool for Firewall Administration -- The B-Method for the Construction of Microkernel-Based Systems -- Hardware Verification and Beyond: Using B at AWE -- Tool Papers -- A JAG Extension for Verifying LTL Properties on B Event Systems -- A Generic Flash-Based Animation Engine for ProB -- BE4: The B Extensible Eclipse Editing Environment -- BRAMA: A New Graphic Animation Tool for B Models -- LEIRIOS Test Generator: Automated Test Generation from B Models.-Meca: A Tool for Access Control Models -- JML2B: Checking JML Specifications with B Machines -- Invited Talk -- Plug-and-Play Nondeterminacy. |
|
|
|
|
|
|
Sommario/riassunto |
|
TheseproceedingsrecordthepaperspresentedattheSeventhInternationalC- ference of B Users (B 2007), held in the city of Besan¸ con in the east of France. This conference was built on the success of the previous six conferences in this series, B 1996, held at the University of Nantes, France; B 1998, held at the University of Montpellier, France; ZB 2000, held at the University of York, UK; ZB 2002, held at the University of Grenoble, France; ZB 2003, held at the U- versity of Turku, Finland; ZB 2005 held at the University of Surrey, Guildford, UK. B 2007 was held in January at the University of Franche-Comt´ e,Besan¸ con, France, hosted by the Computer Science Department (LIFC). LIFC has always placed particular emphasis on the applicability of its research and its relati- ship with industrial partners. In this context, it created in 2003 a company called LEIRIOS Technologies, which produces an automatic test generator tool (LTG) frommodels described in the B speci?cationlanguage. Other members of LIFC work on extensions of the B method for specifying and verifying dynamic properties. All the submitted papers in these proceedings were peer reviewed by at least three reviewers drawn from the B committee, depending on the subject matter of the paper. The authorsof the papersforB 2007werefrom Australia,Canada, Finland, Germany, France, Switzerland, and the UK. The conference featured a rangeof contributions by distinguished invited speakers drawn from both ind- try and academia. |
|
|
|
|
|
|
|
| |