Verified Software. Theories, Tools and Experiments.

Compositional Safety LTL Synthesis.- Leroy and Blazy were right: their memory model soundness proof is automatable.- Shellac: a compiler synthesizer for concurrent programs.- A sequentialization procedure for fault-tolerant protocols.- Towards Practical Partial Order Reduction for High-Level Formalisms.- SMT-based Verification of Persistency Invariants of Px86 Programs.- A Formal Semantics for P-Code.- Separating Separation Logic - Modular Verification of Red-Black Trees.- Residual Runtime Verification via Reachability Analysis.

Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.

• Hardware do computador
• Engenharia do software
• Teoria matemática da computação
• Análise e projecto de sistemas
• Os sistemas especialistas / sistemas baseados em conhecimento
• Inteligência artificial

computer programming;artificial intelligence;software architecture;parallel processing systems;computer systems;architecting;architecture verification and validation;distributed computer systems;distributed systems;embedded systems;engineering;formal logic;linguistics;mathematics;software architecture;software design;software engineering;software quality;verification;verification and validation