[Show/Hide Left Column]


References SciLex Previous Up Next

References SciLex

M. Aiguier, P. Le Gall, and M. Mabrouki. Complex software systems : Formalization and applications. (IARIA) International Journal on Advances in Software, 2(1):47–62, 2009. Invited paper - Extended version of the conference paper ICSEA’08.
L. C. Aleardi, É. Fusy, and T. Lewiner. Schnyder woods for higher genus triangulated surfaces, with applications to encoding. Discrete & Computational Geometry, 42(3):489–516, 2009.
D. Aloise, P. Hansen, and L. Liberti. An improved column generation algorithm for minimum sum-of-squares clustering. Mathematical Programming A, DOI 10.1007/s10107-010-0349-7.
É. André, Th. Chatain, E. Encrenaz, and L. Fribourg. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 20(5):819–836, October 2009.
M. E. Andrés, C. Palamidessi, P. van Rossum, and A. Sokolova. Information hiding in probabilistic concurrent systems. Theor. Comput. Sci., 412(28):3072–3089, 2011.
A. Aristizábal, F. Bonchi, C. Palamidessi, L. Pino, and F. D. Valencia. Deriving labels and bisimilarity for concurrent constraint programming. In M. Hofmann, editor, FOSSACS, volume 6604 of LNCS, pages 138–152. Springer, 2011.
M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry, and B. Werner. A modular integration of sat/smt solvers to coq through proof witnesses. In CPP, LNCS. Springer, 2011.
P. Audebaud and C. Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568–589, 2009.
G. Aupy and O. Bournez. On the number of binary-minded individuals required to compute √1/2. Theoretical Computer Science, 411(22):2262–2267, 2011.
A. Ayad and C. Marché. Multi-prover verification of floating-point programs. In J. Giesl and R. Hähnle, editors, IJCAR, volume 6173 of LNCS, pages 127–141. Springer, 2010.
P. Ayrault, T. Hardin, and F. Pessaux. Development life-cycle of critical software under focal. Electr. Notes Theor. Comput. Sci., 243:15–31, 2009.
P. Ayrault, T. Hardin, and F. Pessaux. Development of a generic voter under focal. In C. Dubois, editor, Tests and Proofs, Third International Conference TAP, volume 5668, pages 10–26, Zurich, Switzerland, 2009.
S. Baarir, M. Beccuti, C. Dutheillet, G. Franceschinis, and S. Haddad. Lumping partially symmetrical stochastic models. Performance Evaluation, 76:21–44, January 2011.
D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu. The Bedwyr system for model checking over syntactic expressions. In F. Pfenning, editor, 21th Conf. on Automated Deduction (CADE), number 4603 in Lecture Notes in Artificial Intelligence, pages 391–397. Springer, 2007.
T. Balabonski and E. Haucourt. A geometric approach to the problem of unique decomposition of processes. In P. Gastin and F. Laroussinie, editors, CONCUR, volume 6269 of LNCS, pages 132–146. Springer, 2010.
P. Baldan, Th. Chatain, S. Haar, and B. König. Unfolding-based diagnosis of systems with an evolving topology. Information and Computation, 208(10):1169–1192, October 2010.
P. Ballarini, H. Djafri, M. Duflot, S. Haddad, and N. Pekergin. HASL : an expressive language for statistical verification of stochastic models. In Proc. 5th Int. Conf. ValueTOOLS’11, 2011. To appear.
B. Bank, M. Giusti, J. Heintz, M. Safey El Din, and E. Schost. On the geometry of polar varieties. Appl. Algebra Engrg. Comm. Comput., 21(1):33–83, 2010.
S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Acceleration from theory to practice. International Journal on Software Tools for Technology Transfer, 10(5):401–424, October 2008.
B. Barras. Sets in Coq, Coq in Sets. Journal of Formalized Reasoning, 3(1):29–48, 2010.
J. Beauquier, J. Burman, J. Clément, and S. Kutten. Brief announcement: non-self-stabilizing and self-stabilizing gathering in networks of mobile agents–the notion of speed. In S. Tirthapura and L. Alvisi, editors, PODC, pages 286–287. ACM, 2009.
J. Beauquier, J. Burman, and S. Kutten. A self-stabilizing transformer for population protocols with covering. Theor. Comput. Sci., 412(33):4247–4259, 2011.
P. Belotti, J. Lee, L. Liberti, F. Margot, and A. Wächter. Branching and bounds tightening techniques for non-convex MINLP. Optimization Methods and Software, 24(4):597–634, 2009.
L. Bentakouk, P. Poizat, and F. Zaïdi. A formal framework for service orchestration testing based on symbolic transition systems. In M. Núñez, P. Baker, and M. G. Merayo, editors, TestCom/FATES, volume 5826 of LNCS, pages 16–32, 2009.
L. Bentakouk, P. Poizat, and F. Zaïdi. Checking the behavioral conformance of web services with symbolic testing and an smt solver. In M. Gogolla and B. Wolff, editors, TAP, volume 6706 of LNCS, pages 33–50. Springer, 2011.
J. Berthomieu, J. v. d. Hoeven, and G. Lecerf. Relaxed algorithms for p-adic numbers. Manuscript to appear in J. Théor. Nombres Bordeaux, 2010.
J. Berthomieu and G. Lecerf. Reduction of bivariate polynomials from convex-dense to dense, with application to factorization. Manuscript to appear in Math. Comp., 2010.
Y. Bertot, F. Guilhot, and A. Mahboubi. A formal study of bernstein coefficients and polynomials. Mathematical Structures in Computer Science, 21(4):731–761, 2011.
D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and Th. A. Henzinger. Alpaga: A tool for solving parity games with imperfect information. In S. Kowalewski and A. Philippou, editors, Proceedings of the 15th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’09), volume 5505 of LNCS, pages 58–61, York, UK, March 2009. Springer.
A. Berzati, C. Canovas-Dumas, and L. Goubin. Public key perturbation of randomized rsa implementations. In CHES, pages 306–319, 2010.
S. Böhme, M. Moskal, W. Schulte, and B. Wolff. HOL-Boogie — An Interactive Prover-Backend for the Verified C Compiler. Journal of Automated Resoning (JAR), 44(1–2):111–144, 2009.
S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, and P. Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In M. Kaufmann and L. C. Paulson, editors, Proceedings of the first Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147–162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOLs and ACL2).
S. Boldo and G. Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In E. Antelo, D. Hough, and P. Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243–252, Tübingen, Germany, 2011.
R. Bonnet. The reachability problem for vector addition systems with one zero-test. In F. Murlak and P. Sankowski, editors, Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS’11), volume 6907 of LNCS, pages 145–157, Warsaw, Poland, August 2011. Springer.
M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel. Attacking and fixing PKCS#11 security tokens. In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS’10), pages 260–269, Chicago, Illinois, USA, October 2010. ACM Press.
O. Bouissou. Proving the correctness of the implementation of a control-command algorithm. In J. Palsberg and Z. Su, editors, SAS, volume 5673 of LNCS, pages 102–119. Springer, 2009.
O. Bouissou, E. Goubault, S. Putot, K. Tekkal, and F. Védrine. Hybridfluctuat: A static analyzer of numerical programs within a continuous environment. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of LNCS, pages 620–626. Springer, 2009.
O. Bournez, D. Graça, and A. Pouly. Solving analytic differential equations in polynomial time over unbounded domains. In Mathematical Foundations of Computer Science, MFCS’11, LNCS, 2011.
O. Bournez, D. S. Graça, and E. Hainry. Robust computations with dynamical systems. In Mathematical Foundations of Computer Science, MFCS’2010, volume 6281 of LNCS, pages 198–208. Springer, 2010.
O. Bournez and I. Potapov. Preface. International Journal of Foundations of Computer Science, Reachability Problems (RP 2009) Special Issue, 22(4), 2011.
C. Boutrous-Saab, D. Coulibaly, S. Haddad, T. Melliti, P. Moreaux, and S. Rampacek. An integrated framework for web services orchestration. International Journal of Web Services Research, 6(4):1–29, September 2009.
M. Bouvel, C. Chauve, M. Mishna, and D. Rossin. Average-case analysis of perfect sorting by reversals. In CPM, pages 314–325, 2009.
P. Bouyer, U. Fahrenberg, K. G. Larsen, and N. Markey. Quantitative analysis of real-time systems using priced timed automata. Communications of the ACM, 54:78–87, September 2011.
P. Bouyer, N. Markey, and O. Sankur. Robust model-checking of timed automata via pumping in channel machines. In U. Fahrenberg and S. Tripakis, editors, Proceedings of the 9th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’11), volume 6919 of LNCS, pages 97–112, Aalborg, Denmark, September 2011. Springer.
A. D. Brucker, L. Brügger, P. Kearney, and B. Wolff. An approach to modular and testable security models of real-world health-care applications. In Proceedings of the ACM Symposium on Access control models and technologies, pages 133–142. ACM, 2011. SACMAT 2011.
A. D. Brucker and B. Wolff. On theorem prover-based testing. Formal Aspects of Computing, 2011. to appear.
L. Castelli Aleardi, O. Devillers, et al. Explicit array-based compact data structures for triangulations. In ISAAC, 2011.
A. Chapoutot and M. Martel. Abstract Simulation: a Static Analysis of Simulink Models. In IEEE International Conference on Embedded Systems and Software (ICESS’09), pages 83–92. IEEE Press, 2009.
G. Chapuy, M. Marcus, and G. Schaeffer. A bijection for rooted maps on orientable surfaces. SIAM J. Discrete Math., 23(3):1587–1611, 2009.
K. Chatterjee and L. Doyen. Energy and mean-payoff parity Markov decision processes. In F. Murlak and P. Sankowski, editors, Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS’11), volume 6907 of LNCS, pages 206–218, Warsaw, Poland, August 2011. Springer.
K. Chatzikokolakis, C. Palamidessi, and P. Panangaden. On the bayes risk in information-hiding protocols. Journal of Computer Security, 16(5):531–571, 2008.
K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz. Verifying safety properties with the TLA+ proof system. In J. Giesl and R. Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of Lecture Notes in Artificial Intelligence, pages 142–148, Edinburgh, UK, July 2010. Springer.
V. Cheval, H. Comon-Lundh, and S. Delaune. Trace equivalence decision: Negative tests and non-determinism. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS’11), Chicago, Illinois, USA, October 2011. ACM Press.
H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS’08), pages 109–118, Alexandria, Virginia, USA, October 2008. ACM Press.
H. Comon-Lundh, V. Cortier, and E. Zălinescu. Deciding security properties for cryptographic protocols. application to key cycles. ACM Transactions on Computational Logic, 11(2), January 2010.
S. Conchon, E. Contejean, and M. Iguernelala. Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. In P. A. Abdulla and K. R. M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS, LNCS, Saarbrücken, Germany, 2011. Springer. EATCS award for ETAPS best paper.
G. Cornuéjols, L. Liberti, and G. Nannicini. Improved strategies for branching on general disjunctions. Mathematical Programming, DOI 10.1007/s10107-009-0333-2.
J.-S. Coron, J. Patarin, and Y. Seurin. The random oracle model and the ideal cipher model are equivalent. In CRYPTO, pages 1–20, 2008.
V. Cortier and S. Kremer, editors. Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series. IOS Press, 2011.
A. Couvreur. Differential approach for the study of duals of algebraic-geometric codes on surfaces. J. Théor. Nombres Bordeaux, 23(1):95–120, 2011.
P. Cuoq, B. Monate, A. Pacalet, and V. Prevosto. Functional dependencies of C functions via weakest pre-conditions. STTT, 13(5):405–417, 2011.
A. Da Costa, F. Laroussinie, and N. Markey. ATL with strategy contexts: Expressiveness and model checking. In K. Lodaya and M. Mahajan, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS’10), volume 8 of Leibniz International Proceedings in Informatics, pages 120–132, Chennai, India, December 2010. Leibniz-Zentrum für Informatik.
M. Daum, J. Dörrenbächer, and B. Wolff. Proving Fairness and Implementation Correctness of a Microkernel Scheduler. Journal of Automated Reasoning (JAR), 42(2–4):349–388, 2009. G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008).
S. Delaune, S. Kremer, and M. D. Ryan. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security, 17(4):435–487, July 2009.
V. Dubois and N. Gama. The degree of regularity of hfe systems. In ASIACRYPT, pages 557–576, 2010.
D. Figueira, S. Figueira, S. Schmitz, and Ph. Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS’11), pages 269–278, Toronto, Canada, June 2011. IEEE Computer Society Press.
J.-C. Filliâtre. Deductive software verification. International Journal on Software Tools for Technology Transfer (STTT), 13(5):397–403, August 2011.
J.-C. Filliâtre and C. Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In W. Damm and H. Hermanns, editors, 19th International Conference on Computer Aided Verification, volume 4590 of LNCS, pages 173–177, Berlin, Germany, July 2007. Springer.
M. Finiasz. Parallel-CFS: Strengthening the CFS McEliece-based signature scheme. In A. Biryukov, G. Gong, and D. Stinson, editors, SAC 2010, volume 6544 of LNCS, pages 161–172. Springer, 2010.
M. Finiasz and N. Sendrier. Security bounds for the design of code-based cryptosystems. In M. Matsui, editor, Asiacrypt 2009, volume 5912 of LNCS, pages 88–105. Springer, 2009.
A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. In S. Albers, A. Marchetti-Spaccamela, Y. Matias, and W. Thomas, editors, ICALP 2009, volume 5556 of LNCS, pages 188–199, Rhodes, Greece, July 2009. Springer.
É. Fusy, G. Schaeffer, and D. Poulalhon. Dissections, orientations, and trees with applications to optimal mesh encoding and random sampling. ACM Transactions on Algorithms, 4(2), 2008.
A. Gacek, D. Miller, and G. Nadathur. A two-level logic approach to reasoning about computations. Accepted to the J. of Automated Reasoning, August 2010.
A. Gacek, D. Miller, and G. Nadathur. Nominal abstraction. Information and Computation, 209(1):48–73, 2011.
F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau. Packaging mathematical structures. In TPHOLs, pages 327–342, 2009.
P. Gastin and D. Kuske. Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Information and Computation, 208(7):797–816, July 2010.
P. Gastin, N. Sznajder, and M. Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design, 34(3):215–237, June 2009.
L. Genelle, E. Prouff, and M. Quisquater. Thwarting higher-order side channel analysis with additive and multiplicative maskings. In CHES, pages 240–255, 2011.
L. George and J. Hermant. A norm approach for the partitioned edf scheduling of sporadic task systems. In Proceedings of 21st Euromicro Conference on Real-Time Systems, ECRTS’09, Dublin, Ireland, July 2009.
G. Gonthier and A. Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2):95–152, 2010.
E. Goubault and E. Haucourt. A practical application of geometric semantics to static analysis of concurrent programs. In M. Abadi and L. de Alfaro, editors, CONCUR, volume 3653 of LNCS, pages 503–517. Springer, 2005.
E. Goubault and E. Haucourt. Components of the fundamental category ii. Applied Categorical Structures, 15(4):387–414, 2007.
E. Goubault and S. Putot. Static analysis of finite precision computations. In VMCAI’11, pages 232–247, 2011.
S. Haar. Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Transactions on Automatic Control, 55(10):2310–2320, October 2010.
G. Hanrot, F. Morain, and E. Thomé, editors. Algorithmic Number Theory, volume 6197 of LNCS. Springer-Verlag, 2010. 9th International Symposium, ANTS-IX, Nancy, France, July 2010, Proceedings.
N. Harrath and B. Monsuez. Systemc waiting state automata. Int. J. Crit. Comput.-Based Syst., 3, February 2012.
J. v. d. Hoeven, G. Lecerf, B. Mourrain, P. Trébuchet, J. Berthomieu, D. N. Diatta, and A. Mantzaflaris. Mathemagix, the quest of modularity and efficiency for symbolic and certified numeric computation. à paraître dans ACM SIGSAM Communications in Computer Algebra.
N. Howgrave-Graham and A. Joux. New generic algorithms for hard knapsacks. In EUROCRYPT, pages 235–256, 2010.
C. Hudelot, J. Atif, and I. Bloch. Integrating bipolar fuzzy mathematical morphology in description logics for spatial reasoning. In ECAI 2010, pages 497–502, Lisbon, Portugal, August 2010.
B. Kanso, M. Aiguier, F. Boulanger, and A. Touil. Testing of abstract components. In ICTAC, pages 184–198, 2010.
M. Kieffer, M. C. Markot, H. Schichl, and E. Walter. Verified global optimization for estimating the parameters of nonlinear models. In E. A. Andreas Rauh, editor, Modeling, Design, and Simulation of Systems with Uncertainties, pages 129–151. Springer-Verlag, June 2011.
M. Kieffer and E. Walter. Guaranteed estimation of the parameters of nonlinear continuous-time models: contributions of interval analysis. Int. J. Adap. Contr. Sig. Proc., 25(3):191–207, February 2010.
M. Kletting, M. Kieffer, and E. Walter. Two Approaches for Guaranteed State Estimation of Nonlinear Continuous-Time Models. In A. R. et E. Auer, editor, Modeling, Design, and Simulation of Systems with Uncertainties, volume 3, pages 199–220. Springer-Verlag, June 2011.
G. Lasnier, T. Robert, L. Pautet, and F. Kordon. Architectural and behavioral modeling with aadl for fault tolerant embedded systems. In ISORC, pages 87–91, Parador of Carmona, Spain, May 2010.
L. Liberti. Reformulations in mathematical programming: Definitions and systematics. RAIRO-RO, 43(1):55–86, 2009.
L. Liberti. Reformulations in mathematical programming: Automatic symmetry detection and exploitation. Mathematical Programming, DOI 10.1007/s10107-010-0351-0.
D. Longuet, M. Aiguier, and P. Le Gall. Proof-guided test selection from first-order specifications with equality. J. Autom. Reasoning, 45(4):437–473, 2010.
M. Marouf and Y. Sorel. Schedulability conditions for non-preemptive hard real-time tasks with strict period. In Proceedings of 18th International Conference on Real-Time and Network Systems, RTNS’10, Toulouse, France, November 2010.
O. Meynard, S. Guilley, J.-L. Danger, Y.-I. Hayashi, and N. Homma. Identification of information leakage points on a cryptographic device with an rsa processor. In EMC, Long Beach, CA, USA, August 2011. IEEE.
F. Nouioua and P. Dague. A probabilistic analysis of diagnosability in discrete event systems. In Proc. of the 18th European Conference on Artificial Intelligence (ECAI-08), July 2008.
F. Ollivier. Jacobi’s Bound and Normal Forms Computations. In L. Guo and W. Y. Sit, editors, Differential Algebra and Related Topics. World Scientific, 2012. to appear.
T. Robert, M. Roy, and J.-C. Fabre. Early error detection for fault tolerance strategies. In International Conference on Real-Time and Network Systems, pages 159–168, France, Toulouse, November 2010. IRIT Press.
L. Sauvage, M. Nassar, S. Guilley, F. Florent, J.-L. Danger, and Y. Mathieu. Exploiting Dual-Output Programmable Blocks to Balance Secure Dual-Rail Logics. International Journal of Reconfigurable Computing, December 2010.
B. Smith. Isogenies and the Discrete Logarithm Problem in Jacobians of Genus 3 Hyperelliptic Curves. Journal of Cryptology, 22(4):505–529, 2009. This is an invited submission to the Journal of Cryptology. It forms an extended version of work that appeared in the proceedings of the Eurocrypt 2008 conference.
B. ten Cate and L. Segoufin. Transitive closure logic, nested tree walking automata, and xpath. J. ACM, 57(3), 2010.
A. Tiu and D. Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2), 2010.
N. Vallée, B. Monsuez, and V.-A. Paun. Extracting Logical Formulae that Capture the Functionality of SystemC Designs. In DATICS-IMECS, volume 2189, Hong-Kong, March 2011. Newswood and International Association of Engineers.
L. Ye and P. Dague. Diagnosability analysis of discrete event systems with autonomous components. In H. Coelho, R. Studer, and M. Wooldridge, editors, ECAI, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 105–110, 2010.
P. M. Yomsi, L. George, Y. Sorel, and D. de Rauglaudre. Improving the quality of control of periodic tasks scheduled by fp with an asynchronous approach. International Journal on Advances in Systems and Measurements, 2(2), 2009.
A. Zeh, C. Gentner, and D. Augot. An interpolation procedure for list decoding reed-Solomon codes based on generalized key equations. Information Theory, IEEE Transactions on, 57(9):5946 –5959, September 2011.
Y. Zhu, E. Westbrook, J. Inoue, A. Chapoutot, C. Salama, M. Peralta, T. Martin, W. Taha, M. O’Malley, R. Cartwright, A. Ames, and R. Bhattacharya. Mathematical Equations as Executable Models of Mechanical Systems. In ACM/IEEE First International Conference of Cyber-Physical Systems (ICCPS’10), pages 1–11, 2010.

Previous Up Next