Filtrer vos résultats
- 40
- 31
- 51
- 13
- 3
- 2
- 1
- 1
- 2
- 70
- 2
- 4
- 8
- 17
- 22
- 12
- 8
- 67
- 2
- 2
- 71
- 71
- 5
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 21
- 16
- 14
- 8
- 7
- 7
- 7
- 6
- 5
- 5
- 4
- 4
- 4
- 3
- 3
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 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
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
71 résultats
|
|
A Refinement-Based Validation Method for Programmable Logic ControllersThe 10th International Conference on Quality Software, Jul 2010, Zhangjiajie, Hunan, China
Communication dans un congrès
inria-00516014v1
|
||
|
|
Modeling and Analysis of Stage Machinery Control Systems by Timed Colored Petri NetsSIES 2008, Jun 2008, Monpellier, France
Communication dans un congrès
inria-00516181v1
|
||
Comparing Learning Algorithms in Automated Assume-Guarantee ReasoningInternational Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2010, Crete, Greece
Communication dans un congrès
inria-00515167v1
|
|||
|
|
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite SystemsIEICE Transactions on Information and Systems, 2009
Article dans une revue
inria-00397820v1
|
||
|
|
Argument filterings and usable rules in higher-order rewrite systems[Research Report] IEICE-TR-SS2010-24.Vol110.N169, 2010
Rapport
inria-00543160v1
|
||
|
|
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant InferenceTACAS 2011 - Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Mar 2011, Saarbruecken, Germany. pp.205-219, ⟨10.1007/978-3-642-19835-9⟩
Communication dans un congrès
hal-00648946v1
|
||
|
|
Proving Computational Geometry Algorithms in TLA+25th IEEE International Conference on Theoretical Aspects of Software Engineering(TASE 2011), Aug 2011, Xi'an, China
Communication dans un congrès
inria-00612413v1
|
||
|
|
CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theoryTwenty-Sixth Annual IEEE Symposium on "Logic in Computer Science" - LICS 2011, Jun 2011, Toronto, Canada
Communication dans un congrès
inria-00583136v1
|
||
|
|
Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilitéLogique [math.LO]. Université Paris-Diderot - Paris VII, 2012
HDR
tel-00724233v2
|
||
|
|
Elements of mathematics and logic for computer program analysisMaster. Institute of Applied Mechanics and Informatics (IAMA) of the Vietnamese Academy of Sciences and Technology (VAST) at Ho Chi Minh City, Vietnam, 2013, pp.37
Cours
cel-00934160v1
|
||
Diagrammatic Confluence and CompletionInternational Conference in Automata, Languages and Programming, Paul Spirakis, Jul 2009, Rhodes, Greece. ⟨10.1007/978-3-642-02930-1_18⟩
Communication dans un congrès
istex
inria-00436070v1
|
|||
Semantics of Intensional Type Theory extended with Decidable Equational TheoriesComputer Science Logic 2013, Aug 2013, Dagstuhl, Germany. pp.653--667, ⟨10.4230/LIPIcs.CSL.2013.653⟩
Communication dans un congrès
hal-00937197v1
|
|||
Edola: A Domain Modeling and Verification Language for PLC SystemsThe Sixth International Conference on Software Engineering (ICSEA 2011), Oct 2011, Barcelona, Spain
Communication dans un congrès
inria-00612416v1
|
|||
|
|
Certification of SAT Solvers in CoqGuangzhou Symposium on Satisfiability in Logic-Based Modeling, Yuping Shen, Institute of Logic and Cognition Sun Yat-sen University, Guangzhou., Sep 2010, Zuhai, China
Communication dans un congrès
inria-00516906v1
|
||
|
|
Coq Modulo Theory - Short PaperLogic In Computer Science (LICS 2010), Jul 2010, Edimbourg, United Kingdom
Communication dans un congrès
inria-00497794v1
|
||
Generation of Executable Representation for Processor Simulation with Dynamic Translation2008 International Conference on Computer Science and Software Engineering, Dec 2008, Wuhan, China. ⟨10.1109/CSSE.2008.635⟩
Communication dans un congrès
hal-00777157v1
|
|||
|
|
Specifying time-sensitive systems with TLA+COMPSAC 2010 : 34th Annual IEEE Computer Software and Applications Conference, Jul 2010, Seoul, South Korea. pp.425-430
Communication dans un congrès
inria-00516164v1
|
||
|
|
The computability path ordering: the end of a quest7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy
Communication dans un congrès
inria-00288209v2
|
||
|
|
Formal Verification of Netlog ProtocolsTASE, Jul 2012, Beijing, China
Communication dans un congrès
hal-00733634v1
|
||
A Comparison of Two SystemC/TLM Semantics for Formal VerificationFormal Methods and Models for Codesign (MEMOCODE), Jun 2008, Anaheim, United States
Communication dans un congrès
inria-00275456v1
|
|||
SimSoC: A SystemC TLM integrated ISS for full system simulationAPCCAS - IEEE Asia-Pacific Conference on Circuits and Systems - 2008, IEEE, Nov 2008, Macau, Macau SAR China. ⟨10.1109/APCCAS.2008.4746381⟩
Communication dans un congrès
hal-00777158v1
|
|||
Data Mining Based Decomposition for Assume-Guarantee Reasoning9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), Sep 2009, Austin, United States
Communication dans un congrès
inria-00517881v1
|
|||
Translation-based model checking for PLC programs33rd Annual IEEE International Computer Software and Applications Conference, Jul 2010, Seattle, Washington, United States
Communication dans un congrès
inria-00497123v1
|
|||
|
|
Introducing Explicit Causality in Object-oriented Hybrid System ModelingMOSIM 2012 - 9th International Conference of Modeling, Optimization and SIMulation, Jun 2012, Bordeaux, France. pp.1-10
Communication dans un congrès
hal-00728581v1
|
||
|
|
Domain-specific modeling and verification language EDOLASoftware Engineering [cs.SE]. Tsinghua university, 2009. Chinese. ⟨NNT : ⟩
Thèse
tel-00516709v1
|
||
|
|
A formal semantics of PLC programs in CoqIEEE Computer Software and Applications, COMPSAC'11, Jul 2011, Munich, Germany
Communication dans un congrès
inria-00601906v1
|
||
|
|
Proof Trick: Small InversionsSecond Coq Workshop, Yves Bertot, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès
inria-00489412v2
|
||
|
|
Certification of an Instruction Set SimulatorSystèmes embarqués. Université de Grenoble, 2013. Français. ⟨NNT : ⟩
Thèse
tel-00937524v1
|
||
|
|
Coq Modulo Theory19th EACSL Annual Conference on Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.529--543, ⟨10.1007/978-3-642-15205-4_40⟩
Communication dans un congrès
inria-00497404v1
|
||
|
|
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificatesMathematical Structures in Computer Science, 2011, 21 (4), pp.827-859. ⟨10.1017/S0960129511000120⟩
Article dans une revue
inria-00543157v1
|