| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996465956103316 |
|
|
Titolo |
Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors) |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin : , : Springer, , [2007] |
|
©2007 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2007.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VIII, 387 p.) |
|
|
|
|
|
|
Collana |
|
Programming and Software Engineering ; ; 4789 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Formal methods (Computer science) |
Software engineering |
|
|
|
|
|
|
|
|
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 -- A System Development Process with Event-B and the Rodin Platform -- Challenges in Software Certification -- Security and Knowledge -- Integrating Formal Methods with System Management -- Formal Engineering of XACML Access Control Policies in VDM++ -- A Verification Framework for Agent Knowledge -- Embedded Systems -- From Model-Based Design to Formal Verification of Adaptive Embedded Systems -- Machine-Assisted Proof Support for Validation Beyond Simulink -- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System -- Testing -- Integrating Specification-Based Review and Testing for Detecting Errors in Programs -- Testing for Refinement in CSP -- Reducing Test Sequence Length Using Invertible Sequences -- Automated Analysis -- Model Checking with SAT-Based Characterization of ACTL Formulas -- Automating Refinement Checking in Probabilistic System Design -- Model Checking in Practice: Analysis of Generic Bootloader Using SPIN -- Model Checking Propositional Projection Temporal Logic Based on SPIN -- Hardware -- A Denotational Semantics for Handel-C Hardware Compilation -- Automatic Generation of Verified Concurrent Hardware -- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking -- Concurrency -- |
|
|
|
|
|
|
|
|
|
|
|
|
|
Efficient Symbolic Execution of Large Quantifications in a Process Algebra -- Formalizing SANE Virtual Processor in Thread Algebra -- Calculating and Composing Progress Properties in Terms of the Leads-to Relation -- Erratum -- Erratum to: Challenges in Software Certification. |
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910698769603321 |
|
|
Autore |
Dodaro Gene L |
|
|
Titolo |
Troubled Asset Relief Program [[electronic resource] ] : status of efforts to address transparency and accountability issues : testimony before the Subcommittee on Oversight and Investigations, Committee on Financial Services, House of Representatives / / statement of Gene L. Dodaro |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
[Washington, D.C.] : , : U.S. Govt. Accountability Office, , [2009] |
|
|
|
|
|
|
|
Descrizione fisica |
|
15 pages : digital, PDF file |
|
|
|
|
|
|
Collana |
|
Testimony ; ; GAO-09-417T |
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Title from title screen (viewed on Mar. 12, 2009). |
"For release on ... February 24, 2009." |
|
|
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references. |
|
|
|
|
|
| |