Publication List of Sébastien Bardin





Thesis

  1. S. Bardin. Vers un Model checking avec Accélération Plate des Systèmes Hétérogènes. PhD dissertation, ENS Cachan, October 2005, 172 pages.

Journal articles

  1. S. Bardin and P. Herrmann. OSMOSE: Automatic Structural Testing of Executables. International Journal of Software Testing, Verification and Reliability (STVR): 21(1), pages 29-54, 2011.     
  2. S. Bardin, A. Finkel, J. Leroux and L. PetrucciFAST: Acceleration from theory to practice.  International Journal on Software Tools for Technology Transfer   (STTT): 10(5), pages 401-424, 2008.  

Conference papers & talks

  1. Q. Plazar, M. Acher, S. Bardin and A. Gotlieb. Efficient and Complete FD-Solving for Extended Array Constraints. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI 2017)                                 
  1. S. Bardin, R. David, JY Marion. Backward-bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes [table 1 corrected] In Proceedings of International Symposium on Security and Privacy (S&P 2017)
  1. M. Marcozzi, M. Delahaye, S. Bardin, N. Kosmatov, V. Prevosto. Generic and Effective Specification of Structural Test Objectives. In Proceedings of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
  1. M. Marcozzi, S. Bardin, M. Delahaye, N. Kosmatov, V. Prevosto. Taming Coverage Criteria Heterogeneity with LTest. In Proceedings of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
  1. Z. Chihani, B. Marre, F. Bobot, S. Bardin. Sharpening Constraint Programming approaches for Bit-Vector Theory. In Proceedings of the 14th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR 2017)
  1. J. Feist, L. Mounier, S. Bardin, R. David, M.-L. Potet. Finding the Needle in the Heap : Combining Static Analysis and Dynamic Symbolic Execution to Trigger Use-After-Free. In Proceedings of the  Software Security, Protection, and Reverse Engineering Workshop (SSPREW 2016)
  1. [talk only] R. David, S. Bardin. Code Deobfuscation : Intertwining Dynamic, Static and Symbolic Approaches. In Black Hat Europe 2016
  2. A. Djoudi, S. Bardin,  É. Goubault . Recovering high-level conditions from binary programs. In Proceedings of the International symposium on Formal Methods (FM 2016)

  3. R. David, S. Bardin, J. Feist, T. D. Ta, L. Mounier, M.-L. Potet, J.-Y. Marion.  Specification of Concretization and Symbolization Policies in Symbolic Execution. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA 21016)
  1. R. David, S. Bardin, T. D. Ta, J. Feist, L. Mounier, M.-L. Potet, J.-Y. Marion. BINSEC/SE : A Dynamic Symbolic Execution Toolkit for Binary-level Analysis. In Proceedings of the 23rd IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER 2016)
      
  2. S. Bardin, M. Delahaye, N. Kosmatov. Enhancing Symbolic Execution for Coverage-Oriented Testing. Proceedings of the 9th Workshop on Constraints in Formal Verification (CFV 2015), colocated with ICCAD 2015.
  1. S. Bardin, M. Delahaye, R. David, N. Kosmatov, M. Papadakis, Y. Le Traon, J.-Y. Marion. Sound and quasi-Complete Detection of Infeasible Test RequirementsIn Proceedings of the 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015)  
                                         
  2.  A. Djoudi, S. Bardin. BINSEC: Binary Code Analysis with Low-Level Regions In Proceedings of the 21st International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2015).  
          
  3. S. Bardin, O. Chebaro, M. Delahaye and N. Kosmatov. An All-in-One Toolkit for automated White-Box Testing. In Proceedings of the 8th Test and Proof Conference (TAP 2014)  (extended version).
     
  4. S. Bardin, N. Kosmatov and F. Cheynier. Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria. In Proceedings of the 7th IEEE International Conference on Software Testing, Verification, and Validation (ICST 2014).   
       
  5. S. Bardin, P. Baufreton, N. Cornuet, P. Herrmann and S. Labbé. Binary-level Testing of Embedded Programs. In Proceedings of the 13th International Conference on Quality Software (QSIC 2013).
       
  6. S. Bardin, A. Gotlieb. FDCC: A Combined Approach for Solving Constraints over Finite Domains and Arrays. In Proceedings of the 7th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR 2012). 
  7. S. Bardin, P. Herrmann, J. Leroux, O. Ly, R. Tabary and A. Vincent. The BINCOA Framework for Binary Code Analysis [tool paper]. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011). 

  8. S. Bardin, P. Herrmann and F. Védrine. Refinement-based CFG Reconstruction from Unstructured Programs. In Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2011).              

  9. S. Bardin, P. Herrmann and F. Perroud. An Alternative to SAT-based Approaches for Bit-Vectors. In Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2010).  (errata)
  10. S. Bardin and P. Herrmann. Pruning the Search Space in Path-based Test Generation. In Proceedings of the 2nd IEEE International Conference on Software Testing, Verification, and Validation (ICST 2009), Denver, USA, April  2009, pages 240-249. IEEE Computer Society.

  11. S. Bardin and P. Herrmann. Structural Testing of Executables. In Proceedings of the 1st IEEE International Conference on Software Testing, Verification, and   Validation (ICST 2008), Lillehammer, Norway, April  2008, pages 22-31. IEEE Computer Society.  (journal version)

  12. S. Bardin, J. Leroux, G. Point. FAST Extended Release [tool paper]. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), Seattle, Washington, USA, August 2006 , LNCS 4144, pages 63-66. Springer. 

  13. S. Bardin, A. Finkel, E. Lozes and A. SangnierFrom Pointer Systems to Counter Systems Using Shape Analysis.  In Proceedings of the 5th International Workshop on Automated Verification of Infinite-State Systems (AVIS'06), Vienna, Austria, April 2006

  14. S. Bardin, A. Finkel, J. Leroux and Ph. SchnoebelenFlat acceleration in symbolic model checking.  In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, ROC, October 2005, LNCS 3707, pages 474-488. Springer.  (journal version)

  15. S. Bardin and A. FinkelComposition of accelerations to verify infinite heterogeneous systems In Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, ROC, October-November 2004, LNCS 3299, pages 248-262. Springer. 

  16. S. Bardin, A. Finkel and J. LerouxFASTer Acceleration of Counter Automata in Practice In Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), Barcelona, Spain, March 2004, LNCS 2988, pages 576-590. Springer.  (extended version).

  17. S. Bardin, A. Finkel and D. NowakToward Symbolic Verification of Programs Handling Pointers In Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Barcelona, Spain, April 2004

  18. S. Bardin, and L. Petrucci. From PNML to counter systems for accelerating Petri nets with FAST. In Proceedings of the Workshop on Interchange Formats for Petri Nets (at ICATPN'2004), pages 26-40, Bologna, Italy, June 2004.

  19. S. Bardin, A. Finkel, J. Leroux and L. PetrucciFAST: Fast Acceleration of Symbolic Transition Systems [tool paper]. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), Boulder, Colorado, USA, July 2003, LNCS 2725, pages 118-121. Springer. (extended version).

Other

  1. A. Djoudi, R. David, J. Feist, S. Bardin and T. Dinh Ta. BINSEC : plate-forme d’analyse de code binaire Actes de la 15e conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2016) 
  2. [talk] S. Bardin. Projet ANR BINSEC : analyse formelle de code binaire pour la sécurité. 15e conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2016)
  3. [talk] S. Bardin, R. Bonichon, R. David, A. Djoudi, B. Farinier, J. Feist, L. Mounier, M.-L. Potet, T. Dihn Ta, F. Védrine. BINSEC: Binary-level Semantic Analysis to the Rescue. RMLL security track 2016 
  4. S. Bardin, M. Delahaye, R. David, N. Kosmatov, M. Papadakis, Y. Le Traon, J.-Y. Marion. Détection sûre et quasi-complète d'objectifs de test infaisables. Actes de la 14e conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2015). 
  5.   S. De Oliveira, V. Prevosto, S. Bardin. Au temps en emporte le C. Actes des 26e Journées Francophones des Langages Applicatifs (JFLA 2015).
  6.   F. Bobot, S. Bardin, B. Marre. CP meets SMT. Workshop CP meets Verification 2014 (CPCAV 2014)
  7.   S. Bardin, F. Cheynier and N. Kosmatov. Exécution symbolique et critères de test avancés. Actes de la 13e conférence sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2014).  
  8.   S. Bardin, A. Gotlieb: A Combined Approach for Constraints over Finite Domains and Arrays. CoRR abs/1312.0200 (2013)      
  9.   S. Bardin, N. Kosmatov and F. Cheynier. Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria. CoRR abs/1308.4045 (2013) 
  10.   S. Bardin, P. Herrmann and F. Védrine. Refinement-based CFG reconstruction from executable code.  GDR-GPL meeting, June, 2011.
  11.   S. Bardin, B. Botella, F. Dadeau, F. Charreteur, A. Gotlieb, B. Marre, C. Michel, M. Rueher and N. Williams. Constraint-based Software Testing.  GDR-GPL meeting, January, 2009.
  12.   S. Bardin, A. Finkel, J. Leroux, L. Petrucci and L. Worobel.  FAST: Users'ManualTechnical Report LSV-10, July 2003. Ens Cachan. 

Back