Filtrer vos résultats
- 24
- 1
- 12
- 8
- 2
- 1
- 1
- 1
- 4
- 1
- 25
- 6
- 5
- 4
- 4
- 5
- 1
- 24
- 1
- 25
- 4
- 3
- 3
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 12
- 6
- 4
- 3
- 3
- 3
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
25 résultats
|
|
|
triés par
|
|
|
Automatic Parallelization and Optimization of Programs by Proof Rewriting[Research Report] RR-6806, INRIA. 2009
Rapport
inria-00355778v3
|
||
|
|
Specification and Verification of Multithreaded Object-Oriented Programs with Separation LogicSoftware Engineering [cs.SE]. Université Nice Sophia Antipolis, 2009. English. ⟨NNT : ⟩
Thèse
tel-00424979v1
|
||
|
|
Permission Specifications for Common Multithreaded Programming PatternsBook in the honor of Henk Barendregt for his 60th birthday, Dec 2007, Nimègue, Netherlands
Communication dans un congrès
inria-00204771v1
|
||
|
|
Abstraction over Public Interfaces[Research Report] RR-5330, INRIA. 2004, pp.21
Rapport
inria-00070670v1
|
||
|
|
Preservation of proof obligations for hybrid verification methods6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), 2008, Cape Town, South Africa
Communication dans un congrès
inria-00332718v1
|
||
|
|
Defining and reasoning about recursive functions: a practical tool for the Coq proof assistantFunctional and Logic Programming (FLOPS'06), 2006, Fuji Susono, Japan
Communication dans un congrès
inria-00564237v1
|
||
|
|
Automatic Parallelization and Optimization of Programs by Proof RewritingStatic Analysis Symposium, Aug 2009, Los Angeles, United States. pp.52-68
Communication dans un congrès
inria-00380528v2
|
||
|
|
A Low-Footprint Java-to-Native Compilation Scheme Using Formal MethodsIn Seventh Smart Card Research and Advanced Application IFIP Conference (CARDIS'06), Apr 2006, Tarragona, Spain
Communication dans un congrès
inria-00113758v1
|
||
|
|
Enforcing High-Level Security Properties For Applets[Research Report] RR-5061, INRIA. 2003
Rapport
inria-00071523v1
|
||
|
|
Union of Reducibility Candidates for Orthogonal Constructor Rewriting2008
Pré-publication, Document de travail
inria-00204710v1
|
||
|
|
Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation LogicInternational Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), Jul 2009, Genova, Italy
Communication dans un congrès
hal-00777577v1
|
||
|
|
Secure Information Flow for a Concurrent Language with SchedulingJournal of Computer Security, 2007, Formal Methods in Security Engineering Workshop (FMSE 04), 16 (6), pp.647 - 689
Article dans une revue
inria-00097395v1
|
||
|
|
Verification of Liveness Properties with JML[Research Report] RR-5331, INRIA. 2004, pp.24
Rapport
inria-00071253v1
|
||
|
|
Combining symbolic execution and model checking to reduce dynamic program analysis overheadRR-5263, INRIA. 2004, pp.31
Rapport
inria-00070735v1
|
||
|
|
Separation logic contracts for a Java-like language with fork/join12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), Jose Meseguer and Grigore Rosu, Jul 2008, Urbana, United States
Communication dans un congrès
inria-00320102v1
|
||
Resource usage protocols for iteratorsThe Journal of Object Technology, 2009, Special Issue Workshops IWACO and FTFJP at ECOOP 08, 8 (4), pp.55-83
Article dans une revue
inria-00410128v1
|
|||
|
|
Reasoning about Java's reentrant locksThe Sixth ASIAN Symposium on Programming Languages and Systems (APLAS 2008), Dec 2008, Bangalore, India
Communication dans un congrès
inria-00320115v1
|
||
|
|
Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems2nd ACM Workshop on Formal Methods in Security Engineering - FMSE'2004, Michael Backes, David Basin, and Michael Waidner, Oct 2004, Washington D.C./USA, pp.13-22, ⟨10.1145/1029133.1029136⟩
Communication dans un congrès
inria-00000632v1
|
||
|
|
Reconstruction de preuves pour les formules quantifiées et ensemblistes[Travaux universitaires] 2006, pp.29-VII
Rapport
inria-00212213v1
|
||
|
|
A structured approach to proving compiler optimizations based on dataflow analysisTypes for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81, ⟨10.1007/11617990⟩
Communication dans un congrès
inria-00289549v1
|
||
|
|
A Certified Lightweight Non-Interference Java Bytecode Verifier2007
Autre publication scientifique
inria-00106182v2
|
||
|
|
Specifying and Checking Protocols of Multithreaded ClassesACM Symposium on Applied Computing (SAC'09), ACM, Mar 2009, Honolulu, United States. pp.587--592, ⟨10.1145/1529282.1529407⟩
Communication dans un congrès
inria-00334527v3
|
||
|
|
The stability problem for verification of concurrent object-oriented programsVerification and Analysis of Multi-threaded Java-like Programs, Sep 2007, Lisbonne, Portugal. pp.52
Communication dans un congrès
inria-00202930v1
|
||
|
|
Factorising temporal specificationsRR-5326, INRIA. 2004, pp.28
Rapport
inria-00070674v1
|
||
|
|
Separation Logic Contracts for a Java-like Language with Fork/Join[Technical Report] RR-6430, INRIA. 2008, pp.101
Rapport
inria-00218114v4
|